1.1 --- a/src/HOL/Tools/hologic.ML	Sat Jan 14 17:45:04 2012 +0100
     1.2 +++ b/src/HOL/Tools/hologic.ML	Sat Jan 14 18:18:06 2012 +0100
     1.3 @@ -255,11 +255,11 @@
     1.4  fun dest_eq (Const ("HOL.eq", _) $ lhs $ rhs) = (lhs, rhs)
     1.5    | dest_eq t = raise TERM ("dest_eq", [t])
     1.6  
     1.7 -fun all_const T = Const ("HOL.All", [T --> boolT] ---> boolT);
     1.8 +fun all_const T = Const ("HOL.All", (T --> boolT) --> boolT);
     1.9  fun mk_all (x, T, P) = all_const T $ absfree (x, T) P;
    1.10  fun list_all (xs, t) = fold_rev (fn (x, T) => fn P => all_const T $ Abs (x, T, P)) xs t;
    1.11  
    1.12 -fun exists_const T = Const ("HOL.Ex", [T --> boolT] ---> boolT);
    1.13 +fun exists_const T = Const ("HOL.Ex", (T --> boolT) --> boolT);
    1.14  fun mk_exists (x, T, P) = exists_const T $ absfree (x, T) P;
    1.15  
    1.16  fun choice_const T = Const("Hilbert_Choice.Eps", (T --> boolT) --> T);
    1.17 @@ -270,14 +270,12 @@
    1.18  (* binary operations and relations *)
    1.19  
    1.20  fun mk_binop c (t, u) =
    1.21 -  let val T = fastype_of t in
    1.22 -    Const (c, [T, T] ---> T) $ t $ u
    1.23 -  end;
    1.24 +  let val T = fastype_of t
    1.25 +  in Const (c, T --> T --> T) $ t $ u end;
    1.26  
    1.27  fun mk_binrel c (t, u) =
    1.28 -  let val T = fastype_of t in
    1.29 -    Const (c, [T, T] ---> boolT) $ t $ u
    1.30 -  end;
    1.31 +  let val T = fastype_of t
    1.32 +  in Const (c, T --> T --> boolT) $ t $ u end;
    1.33  
    1.34  (*destruct the application of a binary operator. The dummyT case is a crude
    1.35    way of handling polymorphic operators.*)
    1.36 @@ -307,7 +305,7 @@
    1.37  fun dest_prodT (Type ("Product_Type.prod", [T1, T2])) = (T1, T2)
    1.38    | dest_prodT T = raise TYPE ("dest_prodT", [T], []);
    1.39  
    1.40 -fun pair_const T1 T2 = Const ("Product_Type.Pair", [T1, T2] ---> mk_prodT (T1, T2));
    1.41 +fun pair_const T1 T2 = Const ("Product_Type.Pair", T1 --> T2 --> mk_prodT (T1, T2));
    1.42  
    1.43  fun mk_prod (t1, t2) =
    1.44    let val T1 = fastype_of t1 and T2 = fastype_of t2 in