diff -r 0a5af667dc75 -r 8534f949548e src/Pure/Syntax/simple_syntax.ML
--- a/src/Pure/Syntax/simple_syntax.ML	Sat Jan 14 16:25:54 2012 +0100
+++ b/src/Pure/Syntax/simple_syntax.ML	Sat Jan 14 16:58:29 2012 +0100
@@ -101,8 +101,7 @@
 val bind = idt --| $$ ".";
 
 fun term env T x =
- ($$ "!!" |-- bind :|-- (fn v =>
-   term (v :: env) propT >> (fn B => Term.all (#2 v) $ lambda (Free v) B)) ||
+ ($$ "!!" |-- 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 ||