diff -r 4b1a63678839 -r 7943b69f0188 src/FOL/fologic.ML
--- a/src/FOL/fologic.ML	Wed Aug 17 16:46:58 2011 +0200
+++ b/src/FOL/fologic.ML	Wed Aug 17 18:05:31 2011 +0200
@@ -76,10 +76,10 @@
   | dest_eq t = raise TERM ("dest_eq", [t])
 
 fun all_const T = Const (@{const_name All}, [T --> oT] ---> oT);
-fun mk_all (Free(x,T),P) = all_const T $ (absfree (x,T,P));
+fun mk_all (Free (x, T), P) = all_const T $ absfree (x, T) P;
 
 fun exists_const T = Const (@{const_name Ex}, [T --> oT] ---> oT);
-fun mk_exists (Free(x,T),P) = exists_const T $ (absfree (x,T,P));
+fun mk_exists (Free (x, T), P) = exists_const T $ absfree (x, T) P;
 
 
 (* binary oprations and relations *)