src/Pure/logic.ML
changeset 56244 3298b7a2795a
parent 56243 2e10a36b8d46
child 56245 84fc7dfa3cd4
--- a/src/Pure/logic.ML	Fri Mar 21 12:34:50 2014 +0100
+++ b/src/Pure/logic.ML	Fri Mar 21 15:12:03 2014 +0100
@@ -323,10 +323,10 @@
 
 (** protected propositions and embedded terms **)
 
-val protectC = Const ("prop", propT --> propT);
+val protectC = Const ("Pure.prop", propT --> propT);
 fun protect t = protectC $ t;
 
-fun unprotect (Const ("prop", _) $ t) = t
+fun unprotect (Const ("Pure.prop", _) $ t) = t
   | unprotect t = raise TERM ("unprotect", [t]);