# HG changeset patch
# User wenzelm
# Date 1191362581 -7200
# Node ID b854842e0b8d92da58edc6f0f2d2c644a873bf26
# Parent  cc55041ca8ba66f6d943d9ff746c08faefa2883e
mark inductive results as internal;

diff -r cc55041ca8ba -r b854842e0b8d 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,