# HG changeset patch
# User berghofe
# Date 1160756617 -7200
# Node ID 3634641f940546c6f65bdfdce116c92eb5ba43fb
# Parent  6f19e5eb3a44ae5a6e5dc6cf23dacdf0368f9bbc
Moved old inductive package to old_inductive_package.ML

diff -r 6f19e5eb3a44 -r 3634641f9405 src/HOL/Tools/inductive_codegen.ML
--- a/src/HOL/Tools/inductive_codegen.ML	Fri Oct 13 18:18:58 2006 +0200
+++ b/src/HOL/Tools/inductive_codegen.ML	Fri Oct 13 18:23:37 2006 +0200
@@ -76,7 +76,7 @@
 fun get_clauses thy s =
   let val {intros, graph, ...} = CodegenData.get thy
   in case Symtab.lookup intros s of
-      NONE => (case InductivePackage.get_inductive thy s of
+      NONE => (case OldInductivePackage.get_inductive thy s of
         NONE => NONE
       | SOME ({names, ...}, {intrs, ...}) =>
           SOME (names, thyname_of_const s thy,
diff -r 6f19e5eb3a44 -r 3634641f9405 src/HOL/Tools/inductive_realizer.ML
--- a/src/HOL/Tools/inductive_realizer.ML	Fri Oct 13 18:18:58 2006 +0200
+++ b/src/HOL/Tools/inductive_realizer.ML	Fri Oct 13 18:23:37 2006 +0200
@@ -347,7 +347,7 @@
     (** realizability predicate **)
 
     val (thy3', ind_info) = thy2 |>
-      InductivePackage.add_inductive_i false true "" false false false
+      OldInductivePackage.add_inductive_i false true "" false false false
         (map Logic.unvarify rlzsets) (map (fn (rintr, intr) =>
           ((Sign.base_name (Thm.name_of_thm intr), strip_all
             (Logic.unvarify rintr)), [])) (rintrs ~~ intrs)) [] |>>
@@ -457,7 +457,7 @@
 fun add_ind_realizers name rsets thy =
   let
     val (_, {intrs, induct, raw_induct, elims, ...}) =
-      (case InductivePackage.get_inductive thy name of
+      (case OldInductivePackage.get_inductive thy name of
          NONE => error ("Unknown inductive set " ^ quote name)
        | SOME info => info);
     val _ $ (_ $ _ $ S) = concl_of (hd intrs);
diff -r 6f19e5eb3a44 -r 3634641f9405 src/HOL/Tools/primrec_package.ML
--- a/src/HOL/Tools/primrec_package.ML	Fri Oct 13 18:18:58 2006 +0200
+++ b/src/HOL/Tools/primrec_package.ML	Fri Oct 13 18:23:37 2006 +0200
@@ -288,7 +288,7 @@
       handle ERROR msg => cat_error msg ("The error(s) above occurred for " ^ s)) strings;
     val rec_ts = map (fn eq => head_of (fst (HOLogic.dest_eq (HOLogic.dest_Trueprop eq)))
       handle TERM _ => primrec_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
   in
     gen_primrec_i note def alt_name (names ~~ eqn_ts' ~~ atts) thy
   end;