anchor.diff:          | Failure _ -> ttac th g
       REPEAT_GTCL
   
  +/// Passes a theorem unchanged to a theorem-tactic.
   let (ALL_THEN : thm_tactical) = I
   
  +/// Theorem-tactical which always fails.
   let (NO_THEN : thm_tactical) = fun ttac th -> failwith "NO_THEN"
   
  +/// Composes a list of theorem-tacticals.
   let EVERY_TCL ttcll =
       itlist (fun t1 t2 -> t1 |> THEN_TCL <| t2) ttcll ALL_THEN;;
   
  +/// Applies the first theorem-tactical in a list that succeeds.
   let FIRST_TCL ttcll =
       end_itlist (fun t1 t2 -> t1 |> ORELSE_TCL <| t2) ttcll;;
   
  
positive.code:         current_goalstack := tl l
          !current_goalstack
  
  let p() = !current_goalstack
  
  let top_realgoal() = 
      match !current_goalstack with
      | (_, ((asl, w) :: _), _) :: _ -> asl, w
      | _ -> failwith "top_realgoal: Unhandled case."
  
  let top_goal() = 
      let asl, w = top_realgoal()
      map (concl << snd) asl, w
  
  let top_thm() = 
      match !current_goalstack with
      | (_, [], f) :: _ -> f null_inst []
      | _ -> failwith "top_thm: Unhandled case."
negative.code:         with
          | Failure _ -> failwith "REFL_TAC"
  
  /// Strips an abstraction from each side of an equational goal.
  let (ABS_TAC : tactic) = 
      fun (asl, w) -> 
          try 
  