# HG changeset patch
# User wenzelm
# Date 1164128863 -3600
# Node ID 8f71e2b3fd92b531f88ab8212c31d752ed12c813
# Parent  cc5095d57da4ed71ec1adf9a7092d2176b434248
simplified Proof.theorem(_i);
moved theorem kinds from PureThy to Thm;

diff -r cc5095d57da4 -r 8f71e2b3fd92 src/Pure/Tools/class_package.ML
--- a/src/Pure/Tools/class_package.ML	Tue Nov 21 18:07:41 2006 +0100
+++ b/src/Pure/Tools/class_package.ML	Tue Nov 21 18:07:43 2006 +0100
@@ -208,8 +208,7 @@
   in
     thy
     |> ProofContext.init
-    |> Proof.theorem_i PureThy.internalK NONE after_qed'
-      ((map (fn t => [(t, [])]) o maps (mk_prop thy)) insts)
+    |> Proof.theorem_i NONE after_qed' ((map (fn t => [(t, [])]) o maps (mk_prop thy)) insts)
   end;
 
 in
@@ -219,7 +218,8 @@
 val axclass_instance_arity_i =
   gen_instance (Logic.mk_arities oo Sign.cert_arity) AxClass.add_arity;
 val axclass_instance_sort =      
-  gen_instance (single oo (Logic.mk_classrel oo AxClass.read_classrel)) AxClass.add_classrel I o single;
+  gen_instance (single oo (Logic.mk_classrel oo AxClass.read_classrel))
+    AxClass.add_classrel I o single;
 
 end;
 
@@ -441,7 +441,7 @@
             ((snd o the_class_data thy) class) tyco) (the_ancestry thy sort)) arities;
       in if bind then
         thy
-        |> PureThy.note_thmss_i (*qualified*) PureThy.internalK [((name, atts), [(thms, [])])]
+        |> PureThy.note_thmss_i (*qualified*) Thm.internalK [((name, atts), [(thms, [])])]
         |> snd
       else
         thy