ORELSE* preserving backtracking information

[jozefg]

At the moment the ORELSE* makes no attempt to preserve backtracking information so in a tactic with a couple of branches like this becomes pretty hard to track from the error messages. It shouldn't be too hard to nicely ask ORELSE to save such information for us.

The naive fix is just to do

  exception OrelseFail of
            {firstFailure : exn,
             secondFailure : exn}
  fun ORELSE_LAZY (tac1, tac2) g =
    tac1 g
    handle exn1 => tac2 () g
                   handle exn2 =>
                          raise OrelseFail {firstFailure = exn1,
                                            secondFailure = exn2}

(better naming left to the imagination)

but this runs the risk of presenting absolutely massive traces to some poor end-user. Another option might be to only catch RefinementFail exceptions and just keep track of the corresponding meta-data or something. Either way we probably should expose this exception through the signature so the end-user can figure out how to format these stack-trace like things.

Cheers,