src/HOL/Tools/function_package/inductive_wrap.ML
changeset 21025 10b0821a4d11
parent 20523 36a59e5d0039
child 21051 c49467a9c1e1
--- a/src/HOL/Tools/function_package/inductive_wrap.ML	Fri Oct 13 18:27:27 2006 +0200
+++ b/src/HOL/Tools/function_package/inductive_wrap.ML	Fri Oct 13 18:28:51 2006 +0200
@@ -64,7 +64,7 @@
             val qdefs = map dest_all_all cdefs
 
             val (thy, {intrs = intrs_gen, elims = [elim_gen], ...}) =
-                InductivePackage.add_inductive_i true (*verbose*)
+                OldInductivePackage.add_inductive_i true (*verbose*)
                                                  false (* dont add_consts *)
                                                  "" (* no altname *)
                                                  false (* no coind *)