# HG changeset patch
# User wenzelm
# Date 1191356608 -7200
# Node ID 2d0fa8f31804f719275dbf6adfdf8806b12f36f9
# Parent  f7093e90f36c0585c5a829cd641d06102f04ed51
tuned internal inductive interface;

diff -r f7093e90f36c -r 2d0fa8f31804 src/HOL/Tools/function_package/inductive_wrap.ML
--- a/src/HOL/Tools/function_package/inductive_wrap.ML	Tue Oct 02 22:23:26 2007 +0200
+++ b/src/HOL/Tools/function_package/inductive_wrap.ML	Tue Oct 02 22:23:28 2007 +0200
@@ -40,16 +40,18 @@
 fun inductive_def defs (((R, T), mixfix), lthy) =
     let
       val ({intrs = intrs_gen, elims = [elim_gen], preds = [ Rdef ], induct, ...}, lthy) =
-          InductivePackage.add_inductive_i (! Toplevel.debug) (*verbose*)
-                                           "" (* no altname *)
-                                           false (* no coind *)
-                                           false (* elims, please *)
-                                           false (* induction thm please *)
-                                           [((R, T), NoSyn)] (* the relation *)
-                                           [] (* no parameters *)
-                                           (map (fn t => (("", []), t)) defs) (* the intros *)
-                                           [] (* no special monos *)
-                                           lthy
+          InductivePackage.add_inductive_i
+            {verbose = ! Toplevel.debug,
+              kind = Thm.theoremK,
+              alt_name = "",
+              coind = false,
+              no_elim = false,
+              no_ind = false}
+            [((R, T), NoSyn)] (* the relation *)
+            [] (* no parameters *)
+            (map (fn t => (("", []), t)) defs) (* the intros *)
+            [] (* no special monos *)
+            lthy
 
       val intrs = map2 (requantify lthy (R, T)) defs intrs_gen
                   
diff -r f7093e90f36c -r 2d0fa8f31804 src/HOL/Tools/inductive_realizer.ML
--- a/src/HOL/Tools/inductive_realizer.ML	Tue Oct 02 22:23:26 2007 +0200
+++ b/src/HOL/Tools/inductive_realizer.ML	Tue Oct 02 22:23:28 2007 +0200
@@ -350,7 +350,8 @@
     (** realizability predicate **)
 
     val (ind_info, thy3') = thy2 |>
-      InductivePackage.add_inductive_global false "" false false false
+      InductivePackage.add_inductive_global {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)))