src/HOL/Tools/inductive_realizer.ML
changeset 21022 3634641f9405
parent 20951 868120282837
child 21395 f34ac19659ae
     1.1 --- a/src/HOL/Tools/inductive_realizer.ML	Fri Oct 13 18:18:58 2006 +0200
     1.2 +++ b/src/HOL/Tools/inductive_realizer.ML	Fri Oct 13 18:23:37 2006 +0200
     1.3 @@ -347,7 +347,7 @@
     1.4      (** realizability predicate **)
     1.5  
     1.6      val (thy3', ind_info) = thy2 |>
     1.7 -      InductivePackage.add_inductive_i false true "" false false false
     1.8 +      OldInductivePackage.add_inductive_i false true "" false false false
     1.9          (map Logic.unvarify rlzsets) (map (fn (rintr, intr) =>
    1.10            ((Sign.base_name (Thm.name_of_thm intr), strip_all
    1.11              (Logic.unvarify rintr)), [])) (rintrs ~~ intrs)) [] |>>
    1.12 @@ -457,7 +457,7 @@
    1.13  fun add_ind_realizers name rsets thy =
    1.14    let
    1.15      val (_, {intrs, induct, raw_induct, elims, ...}) =
    1.16 -      (case InductivePackage.get_inductive thy name of
    1.17 +      (case OldInductivePackage.get_inductive thy name of
    1.18           NONE => error ("Unknown inductive set " ^ quote name)
    1.19         | SOME info => info);
    1.20      val _ $ (_ $ _ $ S) = concl_of (hd intrs);