--- 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)));
--- 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 ***)
--- 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 =>
--- 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);