src/HOL/Tools/inductive_realizer.ML
changeset 31723 f5cafe803b55
parent 31668 a616e56a5ec8
child 31781 861e675f01e6
     1.1 --- a/src/HOL/Tools/inductive_realizer.ML	Thu Jun 18 18:31:14 2009 -0700
     1.2 +++ b/src/HOL/Tools/inductive_realizer.ML	Fri Jun 19 17:23:21 2009 +0200
     1.3 @@ -151,7 +151,7 @@
     1.4      fun is_meta (Const ("all", _) $ Abs (s, _, P)) = is_meta P
     1.5        | is_meta (Const ("==>", _) $ _ $ Q) = is_meta Q
     1.6        | is_meta (Const ("Trueprop", _) $ t) = (case head_of t of
     1.7 -          Const (s, _) => can (InductivePackage.the_inductive ctxt) s
     1.8 +          Const (s, _) => can (Inductive.the_inductive ctxt) s
     1.9          | _ => true)
    1.10        | is_meta _ = false;
    1.11  
    1.12 @@ -277,13 +277,13 @@
    1.13      val inducts = PureThy.get_thms thy (Long_Name.qualify qualifier "inducts");
    1.14      val iTs = OldTerm.term_tvars (prop_of (hd intrs));
    1.15      val ar = length vs + length iTs;
    1.16 -    val params = InductivePackage.params_of raw_induct;
    1.17 -    val arities = InductivePackage.arities_of raw_induct;
    1.18 +    val params = Inductive.params_of raw_induct;
    1.19 +    val arities = Inductive.arities_of raw_induct;
    1.20      val nparms = length params;
    1.21      val params' = map dest_Var params;
    1.22 -    val rss = InductivePackage.partition_rules raw_induct intrs;
    1.23 +    val rss = Inductive.partition_rules raw_induct intrs;
    1.24      val rss' = map (fn (((s, rs), (_, arity)), elim) =>
    1.25 -      (s, (InductivePackage.infer_intro_vars elim arity rs ~~ rs)))
    1.26 +      (s, (Inductive.infer_intro_vars elim arity rs ~~ rs)))
    1.27          (rss ~~ arities ~~ elims);
    1.28      val (prfx, _) = split_last (Long_Name.explode (fst (hd rss)));
    1.29      val tnames = map (fn s => space_implode "_" (s ^ "T" :: vs)) rsets;
    1.30 @@ -307,7 +307,7 @@
    1.31  
    1.32      val ((dummies, dt_info), thy2) =
    1.33        thy1
    1.34 -      |> add_dummies (DatatypePackage.add_datatype
    1.35 +      |> add_dummies (Datatype.add_datatype
    1.36             { strict = false, flat_names = false, quiet = false } (map (Binding.name_of o #2) dts))
    1.37             (map (pair false) dts) []
    1.38        ||> Extraction.add_typeof_eqns_i ty_eqs
    1.39 @@ -348,7 +348,7 @@
    1.40      (** realizability predicate **)
    1.41  
    1.42      val (ind_info, thy3') = thy2 |>
    1.43 -      InductivePackage.add_inductive_global (serial_string ())
    1.44 +      Inductive.add_inductive_global (serial_string ())
    1.45          {quiet_mode = false, verbose = false, kind = Thm.generatedK, alt_name = Binding.empty,
    1.46            coind = false, no_elim = false, no_ind = false, skip_mono = false, fork_mono = false}
    1.47          rlzpreds rlzparams (map (fn (rintr, intr) =>
    1.48 @@ -483,7 +483,7 @@
    1.49  fun add_ind_realizers name rsets thy =
    1.50    let
    1.51      val (_, {intrs, induct, raw_induct, elims, ...}) =
    1.52 -      InductivePackage.the_inductive (ProofContext.init thy) name;
    1.53 +      Inductive.the_inductive (ProofContext.init thy) name;
    1.54      val vss = sort (int_ord o pairself length)
    1.55        (subsets (map fst (relevant_vars (concl_of (hd intrs)))))
    1.56    in