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