diff -r ebde66a71ab0 -r cdff6ef76009 src/HOL/Inductive.thy
--- a/src/HOL/Inductive.thy	Wed May 09 07:53:04 2007 +0200
+++ b/src/HOL/Inductive.thy	Wed May 09 07:53:06 2007 +0200
@@ -21,7 +21,6 @@
   ("Tools/datatype_case.ML")
   ("Tools/datatype_package.ML")
   ("Tools/datatype_codegen.ML")
-  ("Tools/recfun_codegen.ML")
   ("Tools/primrec_package.ML")
 begin
 
@@ -61,7 +60,7 @@
 
 text {* Package setup. *}
 
-use "Tools/old_inductive_package.ML"
+ML {* setmp tolerate_legacy_features true use "Tools/old_inductive_package.ML" *}
 setup OldInductivePackage.setup
 
 theorems basic_monos [mono] =
@@ -90,12 +89,12 @@
   then show P ..
 next
   assume "\<And>P\<Colon>bool. P"
-  then show "False" ..
+  then show False ..
 qed
 
 lemma not_eq_False:
   assumes not_eq: "x \<noteq> y"
-  and eq: "x == y"
+  and eq: "x \<equiv> y"
   shows False
   using not_eq eq by auto
 
@@ -107,9 +106,6 @@
 
 text {* Package setup. *}
 
-use "Tools/recfun_codegen.ML"
-setup RecfunCodegen.setup
-
 use "Tools/datatype_aux.ML"
 use "Tools/datatype_prop.ML"
 use "Tools/datatype_rep_proofs.ML"