anchor.diff:      let MK_COMB(thm1, thm2) =
           let MK_COMB(Sequent(asl1, c1), Sequent(asl2, c2)) = 
               match (c1, c2) with
  -            | Comb(Comb(Const("=", _), l1), r1), Comb(Comb(Const("=", _), l2), r2) -> 
  -                match Choice.get <| type_of l1 with
  -                | Tyapp("fun", [ty; _]) when compare ty (Choice.get <| type_of l2) = 0 -> 
  -                    safe_mk_eq (Comb(l1, l2)) (Comb(r1, r2))
  -                    |> Choice.map (fun tm -> Sequent(term_union asl1 asl2, tm))
  -                | _ -> Choice.failwith "MK_COMB: types do not agree"
  +            | Comb(Comb(Const("=", _), l1), r1), Comb(Comb(Const("=", _), l2), r2) ->
  +                match type_of l1, type_of l2 with
  +                | Success ty1, Success ty2 -> 
  +                    match ty1 with
  +                    | Tyapp("fun", [ty; _]) when compare ty ty2 = 0 -> 
  +                        safe_mk_eq (Comb(l1, l2)) (Comb(r1, r2))
  +                        |> Choice.map (fun tm -> Sequent(term_union asl1 asl2, tm))
  +                    | _ -> Choice.failwith "MK_COMB: types do not agree"
  +                | _ -> Choice.failwith "MK_COMB: not both equations"
               | _ -> Choice.failwith "MK_COMB: not both equations"
           Choice.bind2 (curry MK_COMB) thm1 thm2
       
  
positive.code:                 with Failure _ -> false
  
              if exists (can get_const_type) [absname; repname] then 
                  tuple (Choice2Of2 <| Exception "new_basic_type_definition: Constant(s) already in use")
              elif not(asl = []) then tuple (Choice2Of2 <| Exception "new_basic_type_definition: Assumptions in theorem")
              else 
                  let P, x = 
                      try 
  
negative.code:                 let dth = safe_mk_eq c r |> Choice.map (fun tm -> Sequent([], tm))
                  the_definitions := dth :: (!the_definitions)
                  dth
          | _ -> Choice.failwith "new_basic_definition"
      
      (* ------------------------------------------------------------------------- *)
      (* Handling of type definitions.                                             *)
  