moved Thm.def_name(_optional) to more_thm.ML;
moved old-style Thm.get_def to Drule.get_def;

--- a/src/Pure/drule.ML	Sat Mar 07 21:57:36 2009 +0100
+++ b/src/Pure/drule.ML	Sat Mar 07 22:04:59 2009 +0100
@@ -77,6 +77,7 @@
   val beta_conv: cterm -> cterm -> cterm
   val types_sorts: thm -> (indexname-> typ option) * (indexname-> sort option)
   val flexflex_unique: thm -> thm
+  val get_def: theory -> xstring -> thm
   val store_thm: bstring -> thm -> thm
   val store_standard_thm: bstring -> thm -> thm
   val store_thm_open: bstring -> thm -> thm
@@ -459,6 +460,8 @@
 
 val read_prop = certify o SimpleSyntax.read_prop;
 
+fun get_def thy = Thm.axiom thy o NameSpace.intern (Theory.axiom_space thy) o Thm.def_name;
+
 fun store_thm name th =
   Context.>>> (Context.map_theory_result (PureThy.store_thm (Binding.name name, th)));
 

--- a/src/Pure/more_thm.ML	Sat Mar 07 21:57:36 2009 +0100
+++ b/src/Pure/more_thm.ML	Sat Mar 07 22:04:59 2009 +0100
@@ -55,6 +55,8 @@
   val position_of: thm -> Position.T
   val default_position: Position.T -> thm -> thm
   val default_position_of: thm -> thm -> thm
+  val def_name: string -> string
+  val def_name_optional: string -> string -> string
   val has_name_hint: thm -> bool
   val get_name_hint: thm -> string
   val put_name_hint: string -> thm -> thm
@@ -278,6 +280,8 @@
 
 (** specification primitives **)
 
+(* rules *)
+
 fun add_axiom (b, prop) thy =
   let
     val b' = if Binding.is_empty b
@@ -342,6 +346,14 @@
 val default_position_of = default_position o position_of;
 
 
+(* def_name *)
+
+fun def_name c = c ^ "_def";
+
+fun def_name_optional c "" = def_name c
+  | def_name_optional _ name = name;
+
+
 (* unofficial theorem names *)
 
 fun the_name_hint thm = the (AList.lookup (op =) (Thm.get_tags thm) Markup.nameN);

--- a/src/Pure/thm.ML	Sat Mar 07 21:57:36 2009 +0100
+++ b/src/Pure/thm.ML	Sat Mar 07 22:04:59 2009 +0100
@@ -128,9 +128,6 @@
   val hyps_of: thm -> term list
   val full_prop_of: thm -> term
   val axiom: theory -> string -> thm
-  val def_name: string -> string
-  val def_name_optional: string -> string -> string
-  val get_def: theory -> xstring -> thm
   val axioms_of: theory -> (string * thm) list
   val get_name: thm -> string
   val put_name: string -> thm -> thm
@@ -558,14 +555,6 @@
     | NONE => raise THEORY ("No axiom " ^ quote name, [theory]))
   end;
 
-fun def_name c = c ^ "_def";
-
-fun def_name_optional c "" = def_name c
-  | def_name_optional _ name = name;
-
-fun get_def thy = axiom thy o NameSpace.intern (Theory.axiom_space thy) o def_name;
-
-
 (*return additional axioms of this theory node*)
 fun axioms_of thy =
   map (fn s => (s, axiom thy s)) (Symtab.keys (Theory.axiom_table thy));