diff -r 1a610904bbca -r acf10be7dcca src/ZF/Tools/inductive_package.ML
--- a/src/ZF/Tools/inductive_package.ML	Sat Apr 14 11:05:12 2007 +0200
+++ b/src/ZF/Tools/inductive_package.ML	Sat Apr 14 17:35:52 2007 +0200
@@ -274,7 +274,7 @@
       (Thm.assume A RS elim)
       |> Drule.standard';
   fun mk_cases a = make_cases (*delayed evaluation of body!*)
-    (simpset ()) (read_cterm (Thm.theory_of_thm elim) (a, propT));
+    (simpset ()) (Thm.read_cterm (Thm.theory_of_thm elim) (a, propT));
 
   fun induction_rules raw_induct thy =
    let