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]);