--- a/src/Pure/drule.ML Thu Aug 14 11:55:05 2008 +0200
+++ b/src/Pure/drule.ML Thu Aug 14 16:52:46 2008 +0200
@@ -791,13 +791,13 @@
val term_def = get_axiom "term_def";
in
val protect = Thm.capply (certify Logic.protectC);
- val protectI = store_thm "protectI" (PureThy.kind_rule Thm.internalK (standard
+ val protectI = store_thm "protectI" (Thm.kind_rule Thm.internalK (standard
(Thm.equal_elim (Thm.symmetric prop_def) (Thm.assume A))));
- val protectD = store_thm "protectD" (PureThy.kind_rule Thm.internalK (standard
+ val protectD = store_thm "protectD" (Thm.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 Thm.internalK (standard
+ val termI = store_thm "termI" (Thm.kind_rule Thm.internalK (standard
(Thm.equal_elim (Thm.symmetric term_def) (Thm.forall_intr A (Thm.trivial A)))));
end;