src/Pure/Isar/code.ML

   val abstype_interpretation:
     (string * ((string * sort) list * ((string * ((string * sort) list * typ)) * (string * thm)))
       -> theory -> theory) -> theory -> theory
   val add_eqn: thm -> theory -> theory
   val add_nbe_eqn: thm -> theory -> theory
+  val add_abs_eqn: thm -> theory -> theory
   val add_default_eqn: thm -> theory -> theory
   val add_default_eqn_attribute: attribute
   val add_default_eqn_attrib: Attrib.src
   val add_nbe_default_eqn: thm -> theory -> theory
   val add_nbe_default_eqn_attribute: attribute

     | NONE => Proof_Context.extern_const ctxt c
   end;
 
 
 (* constants *)
-
-fun typ_equiv tys = Type.raw_instance tys andalso Type.raw_instance (swap tys);
 
 fun check_bare_const thy t = case try dest_Const t
  of SOME c_ty => c_ty
   | NONE => error ("Not a constant: " ^ Syntax.string_of_term_global thy t);
 

     val (full_lhs, rhs) = (Logic.dest_equals o Thm.plain_prop_of) thm
       handle TERM _ => bad "Not an equation"
            | THM _ => bad "Not a proper equation";
     val (rep, lhs) = dest_comb full_lhs
       handle TERM _ => bad "Not an abstract equation";
-    val (rep_const, ty) = dest_Const rep;
+    val (rep_const, ty) = dest_Const rep
+      handle TERM _ => bad "Not an abstract equation";
     val (tyco, Ts) = (dest_Type o domain_type) ty
       handle TERM _ => bad "Not an abstract equation"
            | TYPE _ => bad "Not an abstract equation";
     val _ = case some_tyco of SOME tyco' => if tyco = tyco' then ()
           else bad ("Abstract type mismatch:" ^ quote tyco ^ " vs. " ^ quote tyco')

     fun add_const (Const (c, ty)) = insert (op =) (c, Sign.const_typargs thy (c, ty))
       | add_const _ = I
     val add_consts = fold_aterms add_const
   in add_consts rhs o fold add_consts args end;
 
-fun dest_eqn thy =
-  apfst (snd o strip_comb) o Logic.dest_equals o Logic.unvarify_global;
+val dest_eqn = apfst (snd o strip_comb) o Logic.dest_equals o Logic.unvarify_global;
 
 abstype cert = Equations of thm * bool list
   | Projection of term * string
   | Abstract of thm * string
 with

           cert_thm
           |> Local_Defs.expand [snd (get_head thy cert_thm)]
           |> Thm.varifyT_global
           |> Conjunction.elim_balanced (length propers);
         fun abstractions (args, rhs) = (map (rpair NONE) args, (rhs, NONE));
-      in (tyscm, map (abstractions o dest_eqn thy o Thm.prop_of) thms ~~ (map SOME thms ~~ propers)) end
+      in (tyscm, map (abstractions o dest_eqn o Thm.prop_of) thms ~~ (map SOME thms ~~ propers)) end
   | equations_of_cert thy (Projection (t, tyco)) =
       let
         val (_, ((abs, _), _)) = get_abstype_spec thy tyco;
         val tyscm = typscheme_projection thy t;
         val t' = Logic.varify_types_global t;
         fun abstractions (args, rhs) = (map (rpair (SOME abs)) args, (rhs, NONE));
-      in (tyscm, [((abstractions o dest_eqn thy) t', (NONE, true))]) end
+      in (tyscm, [((abstractions o dest_eqn) t', (NONE, true))]) end
   | equations_of_cert thy (Abstract (abs_thm, tyco)) =
       let
         val tyscm = typscheme_abs thy abs_thm;
         val (abs, concrete_thm) = concretify_abs thy tyco abs_thm;
         fun abstractions (args, rhs) = (map (rpair NONE) args, (rhs, (SOME abs)));
       in
-        (tyscm, [((abstractions o dest_eqn thy o Thm.prop_of) concrete_thm,
+        (tyscm, [((abstractions o dest_eqn o Thm.prop_of) concrete_thm,
           (SOME (Thm.varifyT_global abs_thm), true))])
       end;
 
 fun pretty_cert thy (cert as Equations _) =
       (map_filter (Option.map (Display.pretty_thm_global thy o AxClass.overload thy) o fst o snd)