# HG changeset patch
# User wenzelm
# Date 1002997894 -7200
# Node ID 86ac4189a1c1abf40ea312bfd6b86a97c9998b6f
# Parent  c0ca4b89159c2005375825228486d4714de9367a
IsarThy.theorem_i Drule.internalK;

diff -r c0ca4b89159c -r 86ac4189a1c1 src/HOL/Tools/inductive_package.ML
--- a/src/HOL/Tools/inductive_package.ML	Sat Oct 13 20:31:05 2001 +0200
+++ b/src/HOL/Tools/inductive_package.ML	Sat Oct 13 20:31:34 2001 +0200
@@ -594,7 +594,10 @@
     val cprops = map (Thm.cterm_of sign o prep_prop (ProofContext.init thy)) raw_props;
     val atts = map (prep_att thy) raw_atts;
     val thms = map (smart_mk_cases thy ss) cprops;
-  in thy |> IsarThy.have_theorems_i [(((name, atts), map Thm.no_attributes thms), comment)] end;
+  in
+    thy |>
+    IsarThy.have_theorems_i Drule.lemmaK [(((name, atts), map Thm.no_attributes thms), comment)]
+  end;
 
 val inductive_cases =
   gen_inductive_cases Attrib.global_attribute Sign.intern_const ProofContext.read_prop;
diff -r c0ca4b89159c -r 86ac4189a1c1 src/HOL/Tools/recdef_package.ML
--- a/src/HOL/Tools/recdef_package.ML	Sat Oct 13 20:31:05 2001 +0200
+++ b/src/HOL/Tools/recdef_package.ML	Sat Oct 13 20:31:34 2001 +0200
@@ -310,8 +310,8 @@
       error ("No termination condition #" ^ string_of_int i ^
         " in recdef definition of " ^ quote name);
   in
-    thy
-    |> IsarThy.theorem_i (((bname, atts), (HOLogic.mk_Trueprop tc, ([], []))), Comment.none) int
+    thy |> IsarThy.theorem_i Drule.internalK
+      (((bname, atts), (HOLogic.mk_Trueprop tc, ([], []))), Comment.none) int
   end;
 
 val recdef_tc = gen_recdef_tc Attrib.global_attribute Sign.intern_const;
diff -r c0ca4b89159c -r 86ac4189a1c1 src/HOL/Tools/typedef_package.ML
--- a/src/HOL/Tools/typedef_package.ML	Sat Oct 13 20:31:05 2001 +0200
+++ b/src/HOL/Tools/typedef_package.ML	Sat Oct 13 20:31:34 2001 +0200
@@ -216,8 +216,10 @@
 (* typedef_proof interface *)
 
 fun gen_typedef_proof prep_term ((name, typ, set), comment) int thy =
-  let val (_, goal, goal_pat, att) = prepare_typedef prep_term false name typ set thy;
-  in thy |> IsarThy.theorem_i ((("", [att]), (goal, ([goal_pat], []))), comment) int end;
+  let val (_, goal, goal_pat, att) = prepare_typedef prep_term false name typ set thy in
+    thy
+    |> IsarThy.theorem_i Drule.internalK ((("", [att]), (goal, ([goal_pat], []))), comment) int
+  end;
 
 val typedef_proof = gen_typedef_proof read_term;
 val typedef_proof_i = gen_typedef_proof cert_term;
diff -r c0ca4b89159c -r 86ac4189a1c1 src/Pure/axclass.ML
--- a/src/Pure/axclass.ML	Sat Oct 13 20:31:05 2001 +0200
+++ b/src/Pure/axclass.ML	Sat Oct 13 20:31:34 2001 +0200
@@ -440,7 +440,7 @@
 
 fun inst_proof mk_prop add_thms (sig_prop, comment) int thy =
   thy
-  |> IsarThy.theorem_i ((("", [inst_attribute add_thms]),
+  |> IsarThy.theorem_i Drule.internalK ((("", [inst_attribute add_thms]),
     (mk_prop (Theory.sign_of thy) sig_prop, ([], []))), comment) int;
 
 val instance_subclass_proof = inst_proof (mk_classrel oo read_classrel) add_classrel_thms;