tuned;

--- 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 ||

--- a/src/Pure/drule.ML	Sat Jan 14 16:25:54 2012 +0100
+++ b/src/Pure/drule.ML	Sat Jan 14 16:58:29 2012 +0100
@@ -750,19 +750,18 @@
 
 (* HHF normalization *)
 
-(* (PROP ?phi ==> (!!x. PROP ?psi(x))) == (!!x. PROP ?phi ==> PROP ?psi(x)) *)
+(* (PROP ?phi ==> (!!x. PROP ?psi x)) == (!!x. PROP ?phi ==> PROP ?psi x) *)
 val norm_hhf_eq =
   let
     val aT = TFree ("'a", []);
-    val all = Term.all aT;
     val x = Free ("x", aT);
     val phi = Free ("phi", propT);
     val psi = Free ("psi", aT --> propT);
 
     val cx = certify x;
     val cphi = certify phi;
-    val lhs = certify (Logic.mk_implies (phi, all $ Abs ("x", aT, psi $ Bound 0)));
-    val rhs = certify (all $ Abs ("x", aT, Logic.mk_implies (phi, psi $ Bound 0)));
+    val lhs = certify (Logic.mk_implies (phi, Logic.all x (psi $ x)));
+    val rhs = certify (Logic.all x (Logic.mk_implies (phi, psi $ x)));
   in
     Thm.equal_intr
       (Thm.implies_elim (Thm.assume lhs) (Thm.assume cphi)

--- a/src/Pure/primitive_defs.ML	Sat Jan 14 16:25:54 2012 +0100
+++ b/src/Pure/primitive_defs.ML	Sat Jan 14 16:58:29 2012 +0100
@@ -40,7 +40,7 @@
       | check_arg (Const ("TYPE", Type ("itself", [TFree _]))) = true
       | check_arg _ = false;
     fun close_arg (Bound _) t = t
-      | close_arg x t = Term.all (Term.fastype_of x) $ lambda x t;
+      | close_arg x t = Logic.all x t;
 
     val lhs_bads = filter_out check_arg args;
     val lhs_dups = duplicates (op aconv) args;