--- 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,
--- 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);
--- 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;