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