# HG changeset patch
# User wenzelm
# Date 1224770823 -7200
# Node ID d93980a6c3cba495bf08f07e3e91aee923bdac86
# Parent  4693938e9c2a5d6db997ee5bb4147ece472c9beb
Thm.get_def;

diff -r 4693938e9c2a -r d93980a6c3cb src/ZF/Tools/datatype_package.ML
--- 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 =>
diff -r 4693938e9c2a -r d93980a6c3cb src/ZF/Tools/inductive_package.ML
--- 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);