--- a/src/HOL/Tools/hologic.ML Wed Aug 17 16:46:58 2011 +0200
+++ b/src/HOL/Tools/hologic.ML Wed Aug 17 18:05:31 2011 +0200
@@ -183,7 +183,7 @@
| dest_set t = raise TERM ("dest_set", [t]);
fun Collect_const T = Const ("Set.Collect", (T --> boolT) --> mk_setT T);
-fun mk_Collect (a, T, t) = Collect_const T $ absfree (a, T, t);
+fun mk_Collect (a, T, t) = Collect_const T $ absfree (a, T) t;
fun mk_mem (x, A) =
let val setT = fastype_of A in
@@ -258,11 +258,11 @@
| dest_eq t = raise TERM ("dest_eq", [t])
fun all_const T = Const ("HOL.All", [T --> boolT] ---> boolT);
-fun mk_all (x, T, P) = all_const T $ absfree (x, T, P);
+fun mk_all (x, T, P) = all_const T $ absfree (x, T) P;
fun list_all (xs, t) = fold_rev (fn (x, T) => fn P => all_const T $ Abs (x, T, P)) xs t;
fun exists_const T = Const ("HOL.Ex", [T --> boolT] ---> boolT);
-fun mk_exists (x, T, P) = exists_const T $ absfree (x, T, P);
+fun mk_exists (x, T, P) = exists_const T $ absfree (x, T) P;
fun choice_const T = Const("Hilbert_Choice.Eps", (T --> boolT) --> T);