src/HOL/Tools/inductive_realizer.ML
changeset 25977 b0604cd8e5e1
parent 24926 bcb6b098df11
child 26128 fe2d24c26e0c
     1.1 --- a/src/HOL/Tools/inductive_realizer.ML	Fri Jan 25 23:50:33 2008 +0100
     1.2 +++ b/src/HOL/Tools/inductive_realizer.ML	Sat Jan 26 17:08:35 2008 +0100
     1.3 @@ -351,6 +351,7 @@
     1.4  
     1.5      val (ind_info, thy3') = thy2 |>
     1.6        InductivePackage.add_inductive_global {verbose = false, kind = Thm.theoremK,
     1.7 +          group = serial_string (),  (* FIXME pass proper group (!?) *)
     1.8            alt_name = "", coind = false, no_elim = false, no_ind = false}
     1.9          rlzpreds rlzparams (map (fn (rintr, intr) =>
    1.10            ((Sign.base_name (name_of_thm intr), []),