mark inductive results as internal;
authorwenzelm
Wed, 03 Oct 2007 00:03:01 +0200
changeset 24822 b854842e0b8d
parent 24821 cc55041ca8ba
child 24823 bfb619994060
mark inductive results as internal;
src/HOL/Tools/function_package/inductive_wrap.ML
--- a/src/HOL/Tools/function_package/inductive_wrap.ML	Wed Oct 03 00:03:00 2007 +0200
+++ b/src/HOL/Tools/function_package/inductive_wrap.ML	Wed Oct 03 00:03:01 2007 +0200
@@ -42,7 +42,7 @@
       val ({intrs = intrs_gen, elims = [elim_gen], preds = [ Rdef ], induct, ...}, lthy) =
           InductivePackage.add_inductive_i
             {verbose = ! Toplevel.debug,
-              kind = Thm.theoremK,
+              kind = Thm.internalK,
               alt_name = "",
               coind = false,
               no_elim = false,