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 =>