# HG changeset patch
# User wenzelm
# Date 1004561947 -3600
# Node ID 1703de633aaf5771dd2066563b6c849cdf012958
# Parent  c09427e5f55497d3df5d8051f2283254a4b37ba7
IsarThy.theorem_i: no locale;

diff -r c09427e5f554 -r 1703de633aaf src/HOL/Tools/recdef_package.ML
--- a/src/HOL/Tools/recdef_package.ML	Wed Oct 31 21:58:04 2001 +0100
+++ b/src/HOL/Tools/recdef_package.ML	Wed Oct 31 21:59:07 2001 +0100
@@ -310,7 +310,7 @@
       error ("No termination condition #" ^ string_of_int i ^
         " in recdef definition of " ^ quote name);
   in
-    thy |> IsarThy.theorem_i Drule.internalK
+    thy |> IsarThy.theorem_i Drule.internalK None
       (((bname, atts), (HOLogic.mk_Trueprop tc, ([], []))), Comment.none) int
   end;
 
diff -r c09427e5f554 -r 1703de633aaf src/HOL/Tools/typedef_package.ML
--- a/src/HOL/Tools/typedef_package.ML	Wed Oct 31 21:58:04 2001 +0100
+++ b/src/HOL/Tools/typedef_package.ML	Wed Oct 31 21:59:07 2001 +0100
@@ -244,7 +244,8 @@
       prepare_typedef prep_term true name typ set opt_morphs thy;
     val att = #1 o att_result;
   in
-    thy |> IsarThy.theorem_i Drule.internalK ((("", [att]), (goal, ([goal_pat], []))), comment) int
+    thy |> IsarThy.theorem_i Drule.internalK None
+      ((("", [att]), (goal, ([goal_pat], []))), comment) int
   end;
 
 val typedef_proof = gen_typedef_proof read_term;
diff -r c09427e5f554 -r 1703de633aaf src/Pure/axclass.ML
--- a/src/Pure/axclass.ML	Wed Oct 31 21:58:04 2001 +0100
+++ b/src/Pure/axclass.ML	Wed Oct 31 21:59:07 2001 +0100
@@ -423,7 +423,7 @@
 
 fun inst_proof mk_prop add_thms (sig_prop, comment) int thy =
   thy
-  |> IsarThy.theorem_i Drule.internalK ((("", [inst_attribute add_thms]),
+  |> IsarThy.theorem_i Drule.internalK None ((("", [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;