src/Pure/Syntax/simple_syntax.ML

   term1 env T) x
 and term1 env T x =
  (enum2 "==>" (term2 env propT) >> foldr1 Logic.mk_implies ||
   term2 env T) x
 and term2 env T x =
- (equal env "==" ||
+ (equal env ||
   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) =>
-   Const (eq, Term.fastype_of t --> Term.fastype_of u --> propT) $ t $ u)) x
+and equal env x =
+ (term3 env dummyT -- ($$ "==" |-- 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)) ||