--- a/src/Pure/Syntax/simple_syntax.ML Fri Mar 21 15:12:03 2014 +0100
+++ b/src/Pure/Syntax/simple_syntax.ML Fri Mar 21 20:33:56 2014 +0100
@@ -107,12 +107,12 @@
(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 ||