diff -r 5d21a3e7303c -r 5e009a80fe6d src/Pure/Syntax/simple_syntax.ML
--- a/src/Pure/Syntax/simple_syntax.ML	Wed Nov 19 18:15:31 2008 +0100
+++ b/src/Pure/Syntax/simple_syntax.ML	Thu Nov 20 00:03:47 2008 +0100
@@ -18,7 +18,7 @@
 (* scanning tokens *)
 
 val lexicon = Scan.make_lexicon
-  (map Symbol.explode ["!!", "%", "(", ")", ".", "::", "==", "==>", "=?=", "=>", "&&", "CONST"]);
+  (map Symbol.explode ["!!", "%", "(", ")", ".", "::", "==", "==>", "=?=", "=>", "&&&", "CONST"]);
 
 fun read scan s =
   (case
@@ -81,7 +81,7 @@
         | term2
   term2 = term3 == term2
         | term3 =?= term2
-        | term3 && term2
+        | term3 &&& term2
         | term3
   term3 = ident :: typ
         | var :: typ
@@ -111,7 +111,7 @@
   term2 env T) x
 and term2 env T x =
  (equal env "==" || equal env "=?=" ||
-  term3 env propT -- ($$ "&&" |-- term2 env propT) >> Logic.mk_conjunction ||
+  term3 env propT -- ($$ "&&&" |-- term2 env propT) >> Logic.mk_conjunction ||
   term3 env T) x
 and equal env eq x =
  (term3 env dummyT -- ($$ eq |-- term2 env dummyT) >> (fn (t, u) =>