# HG changeset patch
# User berghofe
# Date 1160756931 -7200
# Node ID 10b0821a4d11c369ac9ec0877a8e85b6b33399a5
# Parent  63ab84bb64d1a40eefd133cafdb42e505c48cd33
Moved old inductive package to old_inductive_package.ML

diff -r 63ab84bb64d1 -r 10b0821a4d11 src/HOL/Tools/function_package/inductive_wrap.ML
--- 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 *)
diff -r 63ab84bb64d1 -r 10b0821a4d11 src/HOLCF/fixrec_package.ML
--- a/src/HOLCF/fixrec_package.ML	Fri Oct 13 18:27:27 2006 +0200
+++ b/src/HOLCF/fixrec_package.ML	Fri Oct 13 18:28:51 2006 +0200
@@ -231,7 +231,7 @@
     val eqn_ts = map (prep_prop thy) strings;
     val rec_ts = map (fn eq => chead_of (fst (dest_eqs (Logic.strip_imp_concl eq)))
       handle TERM _ => fixrec_eq_err thy "not a proper equation" eq) eqn_ts;
-    val (_, eqn_ts') = InductivePackage.unify_consts thy rec_ts eqn_ts;
+    val (_, eqn_ts') = OldInductivePackage.unify_consts thy rec_ts eqn_ts;
     
     fun unconcat [] _ = []
       | unconcat (n::ns) xs = List.take (xs,n) :: unconcat ns (List.drop (xs,n));