anchor.diff:  (* ------------------------------------------------------------------------- *)
   
   type goalstate0 = (term list * instantiation) * goal list * justification
  -type goalstate = Choice<goalstate0, exn>
  +type goalstate = Protected<goalstate0>
   
   (* ------------------------------------------------------------------------- *)
   (* A goalstack is just a list of goalstates. Could go for more...            *)
  
positive.code:         }
          |> Choice.mapError (fun e -> nestedFailure e "SPEC_TAC: Failure.")
  
  let private tactic_type_compatibility_check pfx e g =
      choice {
      let! et = type_of e
      let! gt = type_of g
  
negative.code: 
  /// Augments a tactic's theorem list with the assumptions.
  let ASM : (Protected<thm0> list -> tactic) -> Protected<thm0> list -> tactic = 
      fun tltac ths (asl, w as g) ->
          tltac (map snd asl @ ths) g
  
  /// Augments a tactic's theorem list with named assumptions.
  let HYP = 
  