anchor.diff:  
   /// Apply a theorem-tactic to the the first assumption equal to given term.
   let (FIND_ASSUM : thm_tactic -> term -> tactic) = 
  -    fun ttac t ((asl, w) as g) -> ttac (snd(Option.get <| find (fun (_, th) -> concl <| Choice.get th = t) asl)) g
  +    fun ttac t ((asl, w) as g) -> 
  +        choice {
  +            let! asl = Choice.List.map snd asl
  +            return! ttac (Option.toChoiceWithError "find" <| find (fun th -> concl th = t) asl) g
  +        }
   
   /// Applies tactic generated from the first element of a goal's assumption list.
   let (POP_ASSUM : thm_tactic -> tactic) = 
  
positive.code: 
  /// Sequentially applies all the tactics in a given list of tactics.
  let EVERY tacl =
      itlist (fun t1 t2 -> t1 |> THEN <| t2) tacl ALL_TAC
  
  /// Applies the first tactic in a tactic list that succeeds.
  let FIRST : tactic list -> tactic =
      fun tacl g -> end_itlist (fun t1 t2 -> t1 |> ORELSE <| t2) tacl g;;
  
  /// Sequentially applies all tactics given by mapping a function over a list.
  let MAP_EVERY (tacf : 'T -> tactic) (lst : 'T list) : tactic = 
  
negative.code: let (ALL_THEN : thm_tactical) = I
  
  /// Theorem-tactical which always fails.
  let (NO_THEN : thm_tactical) = 
      fun ttac th g -> Choice.failwith "NO_THEN"
  
  /// Composes a list of theorem-tacticals.
  let EVERY_TCL ttcll =
      itlist THEN_TCL ttcll ALL_THEN
  
  /// Applies the first theorem-tactical in a list that succeeds.
  let FIRST_TCL ttcll =
      end_itlist ORELSE_TCL ttcll
  
  (* ------------------------------------------------------------------------- *)
  (* Tactics to augment assumption list. Note that to allow "ASSUME p" for     *)
  