Thm.get_def;

--- a/src/ZF/Tools/datatype_package.ML	Thu Oct 23 15:28:39 2008 +0200
+++ b/src/ZF/Tools/datatype_package.ML	Thu Oct 23 16:07:03 2008 +0200
@@ -303,7 +303,7 @@
 
   (*** Prove the recursor theorems ***)
 
-  val recursor_eqns = case try (get_def thy1) recursor_base_name of
+  val recursor_eqns = case try (Thm.get_def thy1) recursor_base_name of
      NONE => (writeln "  [ No recursion operator ]";
               [])
    | SOME recursor_def =>

--- a/src/ZF/Tools/inductive_package.ML	Thu Oct 23 15:28:39 2008 +0200
+++ b/src/ZF/Tools/inductive_package.ML	Thu Oct 23 16:07:03 2008 +0200
@@ -182,7 +182,7 @@
 
   (*fetch fp definitions from the theory*)
   val big_rec_def::part_rec_defs =
-    map (get_def thy1)
+    map (Thm.get_def thy1)
         (case rec_names of [_] => rec_names
                          | _   => big_rec_base_name::rec_names);