src/ZF/Tools/inductive_package.ML

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