src/Pure/drule.ML
changeset 21437 a3c55b85cf0e
parent 20904 363a9cba2953
child 21519 33f109ea389f
--- a/src/Pure/drule.ML	Tue Nov 21 18:07:32 2006 +0100
+++ b/src/Pure/drule.ML	Tue Nov 21 18:07:33 2006 +0100
@@ -934,13 +934,13 @@
   val term_def = unvarify ProtoPure.term_def;
 in
   val protect = Thm.capply (cert Logic.protectC);
-  val protectI = store_thm "protectI" (PureThy.kind_rule PureThy.internalK (standard
+  val protectI = store_thm "protectI" (PureThy.kind_rule Thm.internalK (standard
       (Thm.equal_elim (Thm.symmetric prop_def) (Thm.assume A))));
-  val protectD = store_thm "protectD" (PureThy.kind_rule PureThy.internalK (standard
+  val protectD = store_thm "protectD" (PureThy.kind_rule Thm.internalK (standard
       (Thm.equal_elim prop_def (Thm.assume (protect A)))));
   val protect_cong = store_standard_thm_open "protect_cong" (Thm.reflexive (protect A));
 
-  val termI = store_thm "termI" (PureThy.kind_rule PureThy.internalK (standard
+  val termI = store_thm "termI" (PureThy.kind_rule Thm.internalK (standard
       (Thm.equal_elim (Thm.symmetric term_def) (Thm.forall_intr A (Thm.trivial A)))));
 end;