# HG changeset patch
# User wenzelm
# Date 1187090420 -7200
# Node ID 6d9b1157b9ab633160f37f7a94a275337caa5b9e
# Parent  dd31811bdf46f065e8b5defef270e830bfb40e1c
tuned;

diff -r dd31811bdf46 -r 6d9b1157b9ab src/Pure/Syntax/simple_syntax.ML
--- a/src/Pure/Syntax/simple_syntax.ML	Tue Aug 14 13:20:19 2007 +0200
+++ b/src/Pure/Syntax/simple_syntax.ML	Tue Aug 14 13:20:20 2007 +0200
@@ -116,12 +116,11 @@
    term (v :: env) propT >> (fn B => Term.all (#2 v) $ lambda (Free v) B)) ||
   term1 env T) x
 and term1 env T x =
- (enum2 "==>" (term2 env propT) >> foldr1 (fn (A, B) => Term.implies $ A $ B) ||
+ (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) >> (fn (A, B) =>
-  Const ("ProtoPure.conjunction", propT --> propT --> propT) $ A $ B) ||
+  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) =>