diff -r 2e10a36b8d46 -r 3298b7a2795a src/Pure/logic.ML
--- 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]);