src/Pure/thm.ML

   val extra_shyps       : thm -> sort list
   val force_strip_shyps : bool ref      (* FIXME tmp (since 1995/08/01) *)
   val strip_shyps       : thm -> thm
   val implies_intr_shyps: thm -> thm
   val get_axiom         : theory -> xstring -> thm
+  val def_name		: string -> string
   val get_def           : theory -> xstring -> thm
   val axioms_of         : theory -> (string * thm) list
 
   (*meta rules*)
   val assume            : cterm -> thm

   val implies_intr_hyps : thm -> thm
   val flexflex_rule     : thm -> thm Seq.seq
   val instantiate       :
     (indexname * ctyp) list * (cterm * cterm) list -> thm -> thm
   val trivial           : cterm -> thm
-  val class_triv        : theory -> class -> thm
+  val class_triv        : Sign.sg -> class -> thm
   val varifyT           : thm -> thm
   val freezeT           : thm -> thm
   val dest_state        : thm * int ->
     (term * term) list * term list * term * term
   val lift_rule         : (thm * int) -> thm -> thm

     (case get_ax (theory :: Theory.ancestors_of theory) of
       Some thm => thm
     | None => raise THEORY ("No axiom " ^ quote name, [theory]))
   end;
 
-fun get_def thy name = get_axiom thy (name ^ "_def");
+fun def_name name = name ^ "_def";
+fun get_def thy = get_axiom thy o def_name;
 
 
 (*return additional axioms of this theory node*)
 fun axioms_of thy =
   map (fn (s, _) => (s, get_axiom thy s))

              hyps = [],
              prop = implies$A$A})
   end;
 
 (*Axiom-scheme reflecting signature contents: "OFCLASS(?'a::c, c_class)" *)
-fun class_triv thy c =
-  let val sign = sign_of thy;
-      val Cterm {sign_ref, t, maxidx, ...} =
-          cterm_of sign (Logic.mk_inclass (TVar (("'a", 0), [c]), c))
-            handle TERM (msg, _) => raise THM ("class_triv: " ^ msg, 0, []);
+fun class_triv sign c =
+  let val Cterm {sign_ref, t, maxidx, ...} =
+    cterm_of sign (Logic.mk_inclass (TVar (("'a", 0), [c]), c))
+      handle TERM (msg, _) => raise THM ("class_triv: " ^ msg, 0, []);
   in
     fix_shyps [] []
       (Thm {sign_ref = sign_ref, 
             der = infer_derivs (Class_triv c, []), 
             maxidx = maxidx,