src/ZF/Tools/inductive_package.ML

   val ctxt1 = ProofContext.init thy1;
 
 
   (*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);
 
 
   (********)