src/HOL/Tools/inductive_realizer.ML
changeset 26128 fe2d24c26e0c
parent 25977 b0604cd8e5e1
child 26336 a0e2b706ce73
     1.1 --- a/src/HOL/Tools/inductive_realizer.ML	Mon Feb 25 12:05:58 2008 +0100
     1.2 +++ b/src/HOL/Tools/inductive_realizer.ML	Mon Feb 25 16:31:15 2008 +0100
     1.3 @@ -350,9 +350,9 @@
     1.4      (** realizability predicate **)
     1.5  
     1.6      val (ind_info, thy3') = thy2 |>
     1.7 -      InductivePackage.add_inductive_global {verbose = false, kind = Thm.theoremK,
     1.8 -          group = serial_string (),  (* FIXME pass proper group (!?) *)
     1.9 -          alt_name = "", coind = false, no_elim = false, no_ind = false}
    1.10 +      InductivePackage.add_inductive_global (serial_string ())
    1.11 +        {verbose = false, kind = Thm.theoremK, alt_name = "",
    1.12 +          coind = false, no_elim = false, no_ind = false}
    1.13          rlzpreds rlzparams (map (fn (rintr, intr) =>
    1.14            ((Sign.base_name (name_of_thm intr), []),
    1.15             subst_atomic rlzpreds' (Logic.unvarify rintr)))