# HG changeset patch
# User wenzelm
# Date 1191356604 -7200
# Node ID 0384f48a806eef39df26f6466adc013445164f48
# Parent  74bc59c2c4a636a92bcb1a281c5b8ba1b0d1ebf0
inductive: mark internal theorems as Thm.internalK;

diff -r 74bc59c2c4a6 -r 0384f48a806e src/HOL/Nominal/nominal_package.ML
--- a/src/HOL/Nominal/nominal_package.ML	Tue Oct 02 19:05:20 2007 +0200
+++ b/src/HOL/Nominal/nominal_package.ML	Tue Oct 02 22:23:24 2007 +0200
@@ -595,7 +595,8 @@
 
     val ({raw_induct = rep_induct, intrs = rep_intrs, ...}, thy4) =
       setmp InductivePackage.quiet_mode false
-        (InductivePackage.add_inductive_global false big_rep_name false true false
+        (InductivePackage.add_inductive_global {verbose = false, kind = Thm.internalK,
+            alt_name = big_rep_name, coind = false, no_elim = true, no_ind = false}
            (map (fn (s, T) => ((s, T --> HOLogic.boolT), NoSyn))
               (rep_set_names' ~~ recTs'))
            [] (map (fn x => (("", []), x)) intr_ts) []) thy3;
@@ -1522,7 +1523,8 @@
     val ({intrs = rec_intrs, elims = rec_elims, raw_induct = rec_induct, ...}, thy11) =
       thy10 |>
       setmp InductivePackage.quiet_mode (!quiet_mode)
-        (InductivePackage.add_inductive_global false big_rec_name false false false
+        (InductivePackage.add_inductive_global {verbose = false, kind = Thm.internalK,
+            alt_name = big_rec_name, coind = false, no_elim = false, no_ind = false}
            (map (fn (s, T) => ((s, T), NoSyn)) (rec_set_names' ~~ rec_set_Ts))
            (map dest_Free rec_fns)
            (map (fn x => (("", []), x)) rec_intr_ts) []) ||>
diff -r 74bc59c2c4a6 -r 0384f48a806e src/HOL/Tools/datatype_abs_proofs.ML
--- a/src/HOL/Tools/datatype_abs_proofs.ML	Tue Oct 02 19:05:20 2007 +0200
+++ b/src/HOL/Tools/datatype_abs_proofs.ML	Tue Oct 02 22:23:24 2007 +0200
@@ -155,7 +155,8 @@
 
     val ({intrs = rec_intrs, elims = rec_elims, ...}, thy1) =
       setmp InductivePackage.quiet_mode (!quiet_mode)
-        (InductivePackage.add_inductive_global false big_rec_name' false false true
+        (InductivePackage.add_inductive_global {verbose = false, kind = Thm.internalK,
+            alt_name = big_rec_name', coind = false, no_elim = false, no_ind = true}
            (map (fn (s, T) => ((s, T), NoSyn)) (rec_set_names' ~~ rec_set_Ts))
            (map dest_Free rec_fns)
            (map (fn x => (("", []), x)) rec_intr_ts) []) thy0;
diff -r 74bc59c2c4a6 -r 0384f48a806e src/HOL/Tools/datatype_rep_proofs.ML
--- a/src/HOL/Tools/datatype_rep_proofs.ML	Tue Oct 02 19:05:20 2007 +0200
+++ b/src/HOL/Tools/datatype_rep_proofs.ML	Tue Oct 02 22:23:24 2007 +0200
@@ -177,7 +177,8 @@
 
     val ({raw_induct = rep_induct, intrs = rep_intrs, ...}, thy2) =
       setmp InductivePackage.quiet_mode (! quiet_mode)
-        (InductivePackage.add_inductive_global false big_rec_name false true false
+        (InductivePackage.add_inductive_global {verbose = false, kind = Thm.internalK,
+            alt_name = big_rec_name, coind = false, no_elim = true, no_ind = false}
            (map (fn s => ((s, UnivT'), NoSyn)) rep_set_names') []
            (map (fn x => (("", []), x)) intr_ts) []) thy1;