anchor.diff:  
   /// Apply higher-order instantiation to a goal.
   let inst_goal : instantiation -> goal -> goal = 
  +    // TODO: to get rid of Choice.get, we have to lift from term to Choice<term, exn> in declaration of goal
       fun p (thms, w) -> map (I ||>> INSTANTIATE_ALL p) thms, Choice.get <| instantiate p w
   
   (* ------------------------------------------------------------------------- *)
  
positive.code: 
  /// Tries to ensure that a tactic is valid.
  let (VALID : tactic -> tactic) = 
      let fake_thm(asl, w) = 
          let asms = itlist (union << hyp << Choice.get << snd) asl []
          mk_fthm(asms, w)
      let false_tm = parse_term @"_FALSITY_"
      fun tac (asl, w) -> 
          tac(asl, w)
          |> Choice.bind (fun ((mvs, i), gls, just as res) ->
              let ths = map fake_thm gls
              let asl', w' = dest_thm <| Choice.get(just null_inst ths)
              let asl'', w'' = inst_goal i (asl, w)
              let maxasms = 
                  itlist (fun (_, th) -> union(insert (concl <| Choice.get th) (hyp <| Choice.get th))) asl'' []
              if aconv w' w'' 
                 && forall (fun t -> exists (aconv t) maxasms) 
                        (subtract asl' [false_tm])
              then Choice.result <| res
              else Choice.failwith "VALID: Invalid tactic")
  
  (* ------------------------------------------------------------------------- *)
  (* Various simple combinators for tactics, identity tactic etc.              *)
  
negative.code: let (REMOVE_THEN : string -> thm_tactic -> tactic) = 
      fun s ttac (asl, w) -> 
          let th =
              match assoc s asl with
              | Some thm -> thm
              | None -> Choice.failwith ("USE_TAC: didn't find assumption " + s)
          let asl1, asl2 = chop_list (index s (map fst asl)) asl
          let asl' = asl1 @ tl asl2
          ttac th (asl', w)
  