anchor.diff:  (* ------------------------------------------------------------------------- *)
   (* Simple "define" function.                                                 *)
   (* ------------------------------------------------------------------------- *)
  +
   /// Defines a general recursive function.
  -let define =
  -  let close_definition_clauses tm =
  -    let avs,bod = strip_forall tm
  -    let cjs = conjuncts bod
  -    let fs =
  -      try map (repeat (Choice.toOption << rator) << Choice.get << lhs << snd << strip_forall) cjs
  -      with Failure _ -> failwith "close_definition_clauses: non-equation"
  -    if length (setify fs) <> 1
  -    then failwith "close_definition_clauses: defining multiple functions" else
  -    let f = hd fs
  -    if mem f avs then failwith "close_definition_clauses: fn quantified" else
  -    let do_clause t =
  -      let lvs,bod = strip_forall t
  -      let fvs = subtract (frees(Choice.get <| lhs bod)) (f::lvs)
  -      SPECL fvs (ASSUME(list_mk_forall(fvs,t)))
  -    let ths = map do_clause cjs
  -    let ajs = map (hd << hyp << Choice.get) ths
  -    let th = ASSUME(list_mk_conj ajs)
  -    f,itlist GEN avs (itlist PROVE_HYP (CONJUNCTS th) (end_itlist CONJ ths))
  -  fun tm ->
  +let define = 
  +    let close_definition_clauses tm = 
  +        let avs, bod = strip_forall tm
  +        let cjs = conjuncts bod
  +        let fs = 
  +            try 
  +                map (repeat(Choice.toOption << rator) << Choice.get << lhs << snd << strip_forall) cjs
  +            with
  +            | Failure _ -> failwith "close_definition_clauses: non-equation"
  +        if length(setify fs) <> 1 then failwith "close_definition_clauses: defining multiple functions"
  +        else 
  +            let f = hd fs
  +            if mem f avs then failwith "close_definition_clauses: fn quantified"
  +            else 
  +                let do_clause t = 
  +                    let lvs, bod = strip_forall t
  +                    let fvs = subtract (frees(Choice.get <| lhs bod)) (f :: lvs)
  +                    SPECL fvs (ASSUME(list_mk_forall(fvs, t)))
  +                let ths = map do_clause cjs
  +                let ajs = map (hd << hyp << Choice.get) ths
  +                let th = ASSUME(list_mk_conj ajs)
  +                f, itlist GEN avs (itlist PROVE_HYP (CONJUNCTS th) (end_itlist CONJ ths))
  +    fun tm -> 
       let tm' = snd(strip_forall tm)
  -    try let th,th' = tryfind (fun th -> Some (th,PART_MATCH Choice.result th tm')) (!the_definitions)
  -                     |> Option.getOrFailWith "tryfind"
  -        if (Choice.isResult << PART_MATCH Choice.result th') (concl <| Choice.get th) then
  -         (warn true "Benign redefinition"; th')
  +    try 
  +        let th, th' = 
  +            tryfind (fun th -> Some(th, PART_MATCH Choice.result th tm')) (!the_definitions) 
  +            |> Option.getOrFailWith "tryfind"
  +        if (Choice.isResult << PART_MATCH Choice.result th')(concl <| Choice.get th) then 
  +            (warn true "Benign redefinition"
  +             th')
           else failwith ""
  -    with Failure _ ->
  -      let f,th = close_definition_clauses tm
  -      let etm = Choice.get <| mk_exists(f,hd(hyp <| Choice.get th))
  -      let th1 = prove_general_recursive_function_exists etm
  -      let th2 = new_specification[fst(Choice.get <| dest_var f)] th1
  -      let g = Choice.get <| mk_mconst(Choice.get <| dest_var f)
  -      let th3 = PROVE_HYP th2 (INST [g,f] th)
  -      the_definitions := th3::(!the_definitions); th3
  +    with
  +    | Failure _ -> 
  +        let f, th = close_definition_clauses tm
  +        let etm = Choice.get <| mk_exists(f, hd(hyp <| Choice.get th))
  +        let th1 = prove_general_recursive_function_exists etm
  +        let th2 = new_specification [fst(Choice.get <| dest_var f)] th1
  +        let g = Choice.get <| mk_mconst(Choice.get <| dest_var f)
  +        let th3 = PROVE_HYP th2 (INST [g, f] th)
  +        the_definitions := th3 :: (!the_definitions)
  +        th3
  
positive.code:     | Abs(x,t) -> headonly f t
      | _ -> true in
  
    let MAIN_ADMISS_TAC (asl,w as gl) =
      let had,args = strip_comb w
      if not(is_const had) then failwith "ADMISS_TAC" else
      let f,fbod = Choice.get <| dest_abs(last args)
      let xtup,bod = Choice.get <| dest_gabs fbod
      let hop,args = strip_comb bod
      match (name_of had,name_of hop) with
        "superadmissible","COND"
            -> APPLY_PROFORMA_TAC SUPERADMISSIBLE_COND gl
      | "superadmissible","_MATCH" when
            name_of(repeat (Choice.toOption << rator) (last args)) = "_SEQPATTERN"
            -> (APPLY_PROFORMA_TAC SUPERADMISSIBLE_MATCH_SEQPATTERN |>THEN<|
                CONV_TAC(ONCE_DEPTH_CONV EXISTS_PAT_CONV)) gl
      | "superadmissible","_MATCH" when
           is_pattern "_UNGUARDED_PATTERN" 2 (last args)
            -> let n = length(fst(strip_exists(Choice.get <| body(Choice.get <| body(last args)))))
               let th = EACK_PROFORMA n SUPERADMISSIBLE_MATCH_UNGUARDED_PATTERN
               (APPLY_PROFORMA_TAC th |>THEN<| CONJ_TAC |>THENL<|
                 [SIMPLIFY_MATCH_WELLDEFINED_TAC; ALL_TAC]) gl
      | "superadmissible","_MATCH" when
           is_pattern "_GUARDED_PATTERN" 3 (last args)
            -> let n = length(fst(strip_exists(Choice.get <| body(Choice.get <| body(last args)))))
               let th = EACK_PROFORMA n SUPERADMISSIBLE_MATCH_GUARDED_PATTERN
               (APPLY_PROFORMA_TAC th |>THEN<| CONJ_TAC |>THENL<|
                 [SIMPLIFY_MATCH_WELLDEFINED_TAC; ALL_TAC]) gl
      // Choice.get is safe to use after is_*
      | "superadmissible",_ when is_comb bod && Choice.get <| rator bod = f -> 
               APPLY_PROFORMA_TAC SUPERADMISSIBLE_TAIL gl
      | "admissible","sum"
            -> APPLY_PROFORMA_TAC ADMISSIBLE_SUM gl
      | "admissible","nsum"
            -> APPLY_PROFORMA_TAC ADMISSIBLE_NSUM gl
      | "admissible","MAP"
            -> APPLY_PROFORMA_TAC ADMISSIBLE_MAP gl
      | "admissible","_MATCH" when
            name_of(repeat (Choice.toOption << rator) (last args)) = "_SEQPATTERN"
            -> (APPLY_PROFORMA_TAC ADMISSIBLE_MATCH_SEQPATTERN |>THEN<|
                CONV_TAC(ONCE_DEPTH_CONV EXISTS_PAT_CONV)) gl
      | "admissible","_MATCH"
            -> APPLY_PROFORMA_TAC ADMISSIBLE_MATCH gl
      | "admissible","_UNGUARDED_PATTERN"
            -> APPLY_PROFORMA_TAC ADMISSIBLE_UNGUARDED_PATTERN gl
      | "admissible","_GUARDED_PATTERN"
            -> APPLY_PROFORMA_TAC ADMISSIBLE_GUARDED_PATTERN gl
      | "admissible",_ when is_abs bod
            -> APPLY_PROFORMA_TAC ADMISSIBLE_LAMBDA gl
      // Choice.get is safe to use after is_*
      | "admissible",_ when is_comb bod && Choice.get <| rator bod = f -> 
              if free_in f (Choice.get <| rand bod) then
                 APPLY_PROFORMA_TAC ADMISSIBLE_NEST gl
               else
                 APPLY_PROFORMA_TAC ADMISSIBLE_BASE gl
      | "admissible",_ when is_comb bod && headonly f bod
            -> APPLY_PROFORMA_TAC ADMISSIBLE_COMB gl
      | _ -> failwith "MAIN_ADMISS_TAC" in
  
    let ADMISS_TAC =
      CONJ_TAC |>ORELSE<|
      MATCH_ACCEPT_TAC ADMISSIBLE_CONST |>ORELSE<|
      MATCH_ACCEPT_TAC SUPERADMISSIBLE_CONST |>ORELSE<|
      MAIN_ADMISS_TAC |>ORELSE<|
      MATCH_MP_TAC ADMISSIBLE_IMP_SUPERADMISSIBLE in
  
  (* ------------------------------------------------------------------------- *)
  (* Instantiate the casewise recursion theorem for existential claim.         *)
  
negative.code:                        (\f x. _MATCH (e f x) (c2 f x))
          ==> admissible(<<) p s
                (\f x:P. _MATCH (e f x) (_SEQPATTERN (c1 f x) (c2 f x)))"),
          REWRITE_TAC [MATCH_SEQPATTERN; ADMISSIBLE_COND])
  
  (* ------------------------------------------------------------------------- *)
  (* Superadmissible generalizations where applicable.                         *)
  