src/HOL/Inductive.thy

   ("Tools/datatype_prop.ML")
   ("Tools/datatype_rep_proofs.ML")
   ("Tools/datatype_abs_proofs.ML")
   ("Tools/datatype_case.ML")
   ("Tools/datatype_package.ML")
+  ("Tools/old_primrec_package.ML")
   ("Tools/primrec_package.ML")
   ("Tools/datatype_codegen.ML")
 begin
 
 subsection {* Least and greatest fixed points *}

 use "Tools/datatype_rep_proofs.ML"
 use "Tools/datatype_abs_proofs.ML"
 use "Tools/datatype_case.ML"
 use "Tools/datatype_package.ML"
 setup DatatypePackage.setup
+use "Tools/old_primrec_package.ML"
 use "Tools/primrec_package.ML"
 
 use "Tools/datatype_codegen.ML"
 setup DatatypeCodegen.setup