tuned internal inductive interface;
authorwenzelm
Tue Oct 02 22:23:28 2007 +0200 (2007-10-02)
changeset 248162d0fa8f31804
parent 24815 f7093e90f36c
child 24817 636b23afee76
tuned internal inductive interface;
src/HOL/Tools/function_package/inductive_wrap.ML
src/HOL/Tools/inductive_realizer.ML
     1.1 --- a/src/HOL/Tools/function_package/inductive_wrap.ML	Tue Oct 02 22:23:26 2007 +0200
     1.2 +++ b/src/HOL/Tools/function_package/inductive_wrap.ML	Tue Oct 02 22:23:28 2007 +0200
     1.3 @@ -40,16 +40,18 @@
     1.4  fun inductive_def defs (((R, T), mixfix), lthy) =
     1.5      let
     1.6        val ({intrs = intrs_gen, elims = [elim_gen], preds = [ Rdef ], induct, ...}, lthy) =
     1.7 -          InductivePackage.add_inductive_i (! Toplevel.debug) (*verbose*)
     1.8 -                                           "" (* no altname *)
     1.9 -                                           false (* no coind *)
    1.10 -                                           false (* elims, please *)
    1.11 -                                           false (* induction thm please *)
    1.12 -                                           [((R, T), NoSyn)] (* the relation *)
    1.13 -                                           [] (* no parameters *)
    1.14 -                                           (map (fn t => (("", []), t)) defs) (* the intros *)
    1.15 -                                           [] (* no special monos *)
    1.16 -                                           lthy
    1.17 +          InductivePackage.add_inductive_i
    1.18 +            {verbose = ! Toplevel.debug,
    1.19 +              kind = Thm.theoremK,
    1.20 +              alt_name = "",
    1.21 +              coind = false,
    1.22 +              no_elim = false,
    1.23 +              no_ind = false}
    1.24 +            [((R, T), NoSyn)] (* the relation *)
    1.25 +            [] (* no parameters *)
    1.26 +            (map (fn t => (("", []), t)) defs) (* the intros *)
    1.27 +            [] (* no special monos *)
    1.28 +            lthy
    1.29  
    1.30        val intrs = map2 (requantify lthy (R, T)) defs intrs_gen
    1.31                    
     2.1 --- a/src/HOL/Tools/inductive_realizer.ML	Tue Oct 02 22:23:26 2007 +0200
     2.2 +++ b/src/HOL/Tools/inductive_realizer.ML	Tue Oct 02 22:23:28 2007 +0200
     2.3 @@ -350,7 +350,8 @@
     2.4      (** realizability predicate **)
     2.5  
     2.6      val (ind_info, thy3') = thy2 |>
     2.7 -      InductivePackage.add_inductive_global false "" false false false
     2.8 +      InductivePackage.add_inductive_global {verbose = false, kind = Thm.theoremK,
     2.9 +          alt_name = "", coind = false, no_elim = false, no_ind = false}
    2.10          rlzpreds rlzparams (map (fn (rintr, intr) =>
    2.11            ((Sign.base_name (name_of_thm intr), []),
    2.12             subst_atomic rlzpreds' (Logic.unvarify rintr)))