# HG changeset patch
# User wenzelm
# Date 1266608388 -3600
# Node ID b625eb708d9434c9de3865ebec94e752f4aae938
# Parent  fd8231b16203c8a4c4de547eb1dcbf4cd1855150
moved ancient Drule.get_def to OldGoals.get_def;

diff -r fd8231b16203 -r b625eb708d94 src/Pure/drule.ML
--- a/src/Pure/drule.ML	Fri Feb 19 17:37:33 2010 +0100
+++ b/src/Pure/drule.ML	Fri Feb 19 20:39:48 2010 +0100
@@ -77,7 +77,6 @@
   val flexflex_unique: thm -> thm
   val export_without_context: thm -> thm
   val export_without_context_open: thm -> thm
-  val get_def: theory -> xstring -> thm
   val store_thm: binding -> thm -> thm
   val store_standard_thm: binding -> thm -> thm
   val store_thm_open: binding -> thm -> thm
@@ -451,8 +450,6 @@
 
 val read_prop = certify o Simple_Syntax.read_prop;
 
-fun get_def thy = Thm.axiom thy o Name_Space.intern (Theory.axiom_space thy) o Thm.def_name;
-
 fun store_thm name th =
   Context.>>> (Context.map_theory_result (PureThy.store_thm (name, th)));
 
diff -r fd8231b16203 -r b625eb708d94 src/Pure/old_goals.ML
--- a/src/Pure/old_goals.ML	Fri Feb 19 17:37:33 2010 +0100
+++ b/src/Pure/old_goals.ML	Fri Feb 19 20:39:48 2010 +0100
@@ -16,6 +16,7 @@
   val simple_read_term: theory -> typ -> string -> term
   val read_term: theory -> string -> term
   val read_prop: theory -> string -> term
+  val get_def: theory -> xstring -> thm
   type proof
   val premises: unit -> thm list
   val reset_goals: unit -> unit
@@ -220,6 +221,8 @@
 fun read_prop thy = simple_read_term thy propT;
 
 
+fun get_def thy = Thm.axiom thy o Name_Space.intern (Theory.axiom_space thy) o Thm.def_name;
+
 
 (*** Goal package ***)
 
diff -r fd8231b16203 -r b625eb708d94 src/ZF/Tools/datatype_package.ML
--- a/src/ZF/Tools/datatype_package.ML	Fri Feb 19 17:37:33 2010 +0100
+++ b/src/ZF/Tools/datatype_package.ML	Fri Feb 19 20:39:48 2010 +0100
@@ -298,7 +298,7 @@
 
   (*** Prove the recursor theorems ***)
 
-  val recursor_eqns = case try (Drule.get_def thy1) recursor_base_name of
+  val recursor_eqns = case try (OldGoals.get_def thy1) recursor_base_name of
      NONE => (writeln "  [ No recursion operator ]";
               [])
    | SOME recursor_def =>
diff -r fd8231b16203 -r b625eb708d94 src/ZF/Tools/inductive_package.ML
--- a/src/ZF/Tools/inductive_package.ML	Fri Feb 19 17:37:33 2010 +0100
+++ b/src/ZF/Tools/inductive_package.ML	Fri Feb 19 20:39:48 2010 +0100
@@ -179,7 +179,7 @@
 
   (*fetch fp definitions from the theory*)
   val big_rec_def::part_rec_defs =
-    map (Drule.get_def thy1)
+    map (OldGoals.get_def thy1)
         (case rec_names of [_] => rec_names
                          | _   => big_rec_base_name::rec_names);