diff -r 17874d43d3b3 -r 5348bea4accd src/Pure/Syntax/simple_syntax.ML
--- a/src/Pure/Syntax/simple_syntax.ML	Sun Feb 25 12:59:08 2018 +0100
+++ b/src/Pure/Syntax/simple_syntax.ML	Sun Feb 25 15:44:46 2018 +0100
@@ -17,7 +17,7 @@
 (* scanning tokens *)
 
 val lexicon = Scan.make_lexicon
-  (map Symbol.explode ["!!", "%", "(", ")", ".", "::", "==", "==>", "=>", "&&&", "CONST"]);
+  (map Symbol.explode ["\<And>", "\<lambda>", "(", ")", ".", "::", "\<equiv>", "\<Longrightarrow>", "\<Rightarrow>", "&&&", "CONST"]);
 
 fun read scan s =
   (case
@@ -53,7 +53,7 @@
 (* types *)
 
 (*
-  typ  = typ1 => ... => typ1
+  typ  = typ1 \<Rightarrow> ... \<Rightarrow> typ1
        | typ1
   typ1 = typ2 const ... const
        | typ2
@@ -63,7 +63,7 @@
 *)
 
 fun typ x =
- (enum1 "=>" typ1 >> (op ---> o split_last)) x
+ (enum1 "\<Rightarrow>" typ1 >> (op ---> o split_last)) x
 and typ1 x =
  (typ2 -- Scan.repeat const >> (fn (T, cs) => fold (fn c => fn U => Type (c, [U])) cs T)) x
 and typ2 x =
@@ -77,17 +77,17 @@
 (* terms *)
 
 (*
-  term  = !!ident :: typ. term
+  term  = \<And>ident :: typ. term
         | term1
-  term1 = term2 ==> ... ==> term2
+  term1 = term2 \<Longrightarrow> ... \<Longrightarrow> term2
         | term2
-  term2 = term3 == term2
+  term2 = term3 \<equiv> term2
         | term3 &&& term2
         | term3
   term3 = ident :: typ
         | var :: typ
         | CONST const :: typ
-        | %ident :: typ. term3
+        | \<lambda>ident :: typ. term3
         | term4
   term4 = term5 ... term5
         | term5
@@ -104,23 +104,23 @@
 val bind = idt --| $$ ".";
 
 fun term env T x =
- ($$ "!!" |-- bind :|-- (fn v => term (v :: env) propT >> (Logic.all (Free v))) ||
+ ($$ "\<And>" |-- bind :|-- (fn v => term (v :: env) propT >> (Logic.all (Free v))) ||
   term1 env T) x
 and term1 env T x =
- (enum2 "==>" (term2 env propT) >> foldr1 Logic.mk_implies ||
+ (enum2 "\<Longrightarrow>" (term2 env propT) >> foldr1 Logic.mk_implies ||
   term2 env T) x
 and term2 env T x =
  (equal env ||
   term3 env propT -- ($$ "&&&" |-- term2 env propT) >> Logic.mk_conjunction ||
   term3 env T) x
 and equal env x =
- (term3 env dummyT -- ($$ "==" |-- term2 env dummyT) >> (fn (t, u) =>
+ (term3 env dummyT -- ($$ "\<equiv>" |-- term2 env dummyT) >> (fn (t, u) =>
    Const ("Pure.eq", Term.fastype_of t --> Term.fastype_of u --> propT) $ t $ u)) x
 and term3 env T x =
  (idt >> Free ||
   var -- constraint >> Var ||
   $$ "CONST" |-- const -- constraint >> Const ||
-  $$ "%" |-- bind :|-- (fn v => term3 (v :: env) dummyT >> lambda (Free v)) ||
+  $$ "\<lambda>" |-- bind :|-- (fn v => term3 (v :: env) dummyT >> lambda (Free v)) ||
   term4 env T) x
 and term4 env T x =
  (term5 env dummyT -- Scan.repeat1 (term5 env dummyT) >> Term.list_comb ||
@@ -132,7 +132,10 @@
   $$ "(" |-- term env T --| $$ ")") x;
 
 fun read_tm T s =
-  let val t = read (term [] T) s in
+  let
+    val t = read (term [] T) s
+      handle ERROR msg => cat_error ("Malformed input " ^ quote s) msg;
+  in
     if can (Term.map_types Term.no_dummyT) t then t
     else error ("Unspecified types in input: " ^ quote s)
   end;