Moved old inductive package to old_inductive_package.ML
authorberghofe
Fri Oct 13 18:23:37 2006 +0200 (2006-10-13)
changeset 210223634641f9405
parent 21021 6f19e5eb3a44
child 21023 d559870306f4
Moved old inductive package to old_inductive_package.ML
src/HOL/Tools/inductive_codegen.ML
src/HOL/Tools/inductive_realizer.ML
src/HOL/Tools/primrec_package.ML
     1.1 --- a/src/HOL/Tools/inductive_codegen.ML	Fri Oct 13 18:18:58 2006 +0200
     1.2 +++ b/src/HOL/Tools/inductive_codegen.ML	Fri Oct 13 18:23:37 2006 +0200
     1.3 @@ -76,7 +76,7 @@
     1.4  fun get_clauses thy s =
     1.5    let val {intros, graph, ...} = CodegenData.get thy
     1.6    in case Symtab.lookup intros s of
     1.7 -      NONE => (case InductivePackage.get_inductive thy s of
     1.8 +      NONE => (case OldInductivePackage.get_inductive thy s of
     1.9          NONE => NONE
    1.10        | SOME ({names, ...}, {intrs, ...}) =>
    1.11            SOME (names, thyname_of_const s thy,
     2.1 --- a/src/HOL/Tools/inductive_realizer.ML	Fri Oct 13 18:18:58 2006 +0200
     2.2 +++ b/src/HOL/Tools/inductive_realizer.ML	Fri Oct 13 18:23:37 2006 +0200
     2.3 @@ -347,7 +347,7 @@
     2.4      (** realizability predicate **)
     2.5  
     2.6      val (thy3', ind_info) = thy2 |>
     2.7 -      InductivePackage.add_inductive_i false true "" false false false
     2.8 +      OldInductivePackage.add_inductive_i false true "" false false false
     2.9          (map Logic.unvarify rlzsets) (map (fn (rintr, intr) =>
    2.10            ((Sign.base_name (Thm.name_of_thm intr), strip_all
    2.11              (Logic.unvarify rintr)), [])) (rintrs ~~ intrs)) [] |>>
    2.12 @@ -457,7 +457,7 @@
    2.13  fun add_ind_realizers name rsets thy =
    2.14    let
    2.15      val (_, {intrs, induct, raw_induct, elims, ...}) =
    2.16 -      (case InductivePackage.get_inductive thy name of
    2.17 +      (case OldInductivePackage.get_inductive thy name of
    2.18           NONE => error ("Unknown inductive set " ^ quote name)
    2.19         | SOME info => info);
    2.20      val _ $ (_ $ _ $ S) = concl_of (hd intrs);
     3.1 --- a/src/HOL/Tools/primrec_package.ML	Fri Oct 13 18:18:58 2006 +0200
     3.2 +++ b/src/HOL/Tools/primrec_package.ML	Fri Oct 13 18:23:37 2006 +0200
     3.3 @@ -288,7 +288,7 @@
     3.4        handle ERROR msg => cat_error msg ("The error(s) above occurred for " ^ s)) strings;
     3.5      val rec_ts = map (fn eq => head_of (fst (HOLogic.dest_eq (HOLogic.dest_Trueprop eq)))
     3.6        handle TERM _ => primrec_eq_err thy "not a proper equation" eq) eqn_ts;
     3.7 -    val (_, eqn_ts') = InductivePackage.unify_consts thy rec_ts eqn_ts
     3.8 +    val (_, eqn_ts') = OldInductivePackage.unify_consts thy rec_ts eqn_ts
     3.9    in
    3.10      gen_primrec_i note def alt_name (names ~~ eqn_ts' ~~ atts) thy
    3.11    end;