diff -r a89f876731c5 -r 696d64ed85da src/FOL/fologic.ML
--- a/src/FOL/fologic.ML	Sat Aug 29 10:50:04 2009 +0200
+++ b/src/FOL/fologic.ML	Sat Aug 29 12:01:25 2009 +0200
@@ -6,28 +6,28 @@
 
 signature FOLOGIC =
 sig
-  val oT		: typ
-  val mk_Trueprop	: term -> term
-  val dest_Trueprop	: term -> term
-  val not		: term
-  val conj		: term
-  val disj		: term
-  val imp		: term
-  val iff		: term
-  val mk_conj		: term * term -> term
-  val mk_disj		: term * term -> term
-  val mk_imp		: term * term -> term
-  val dest_imp	       	: term -> term*term
-  val dest_conj         : term -> term list
-  val mk_iff		: term * term -> term
-  val dest_iff	       	: term -> term*term
-  val all_const		: typ -> term
-  val mk_all		: term * term -> term
-  val exists_const	: typ -> term
-  val mk_exists		: term * term -> term
-  val eq_const		: typ -> term
-  val mk_eq		: term * term -> term
-  val dest_eq 		: term -> term*term
+  val oT: typ
+  val mk_Trueprop: term -> term
+  val dest_Trueprop: term -> term
+  val not: term
+  val conj: term
+  val disj: term
+  val imp: term
+  val iff: term
+  val mk_conj: term * term -> term
+  val mk_disj: term * term -> term
+  val mk_imp: term * term -> term
+  val dest_imp: term -> term * term
+  val dest_conj: term -> term list
+  val mk_iff: term * term -> term
+  val dest_iff: term -> term * term
+  val all_const: typ -> term
+  val mk_all: term * term -> term
+  val exists_const: typ -> term
+  val mk_exists: term * term -> term
+  val eq_const: typ -> term
+  val mk_eq: term * term -> term
+  val dest_eq: term -> term * term
   val mk_binop: string -> term * term -> term
   val mk_binrel: string -> term * term -> term
   val dest_bin: string -> typ -> term -> term * term
@@ -46,7 +46,8 @@
 fun dest_Trueprop (Const ("Trueprop", _) $ P) = P
   | dest_Trueprop t = raise TERM ("dest_Trueprop", [t]);
 
-(** Logical constants **)
+
+(* Logical constants *)
 
 val not = Const ("Not", oT --> oT);
 val conj = Const("op &", [oT,oT]--->oT);
@@ -80,6 +81,7 @@
 fun exists_const T = Const ("Ex", [T --> oT] ---> oT);
 fun mk_exists (Free(x,T),P) = exists_const T $ (absfree (x,T,P));
 
+
 (* binary oprations and relations *)
 
 fun mk_binop c (t, u) =
@@ -97,5 +99,4 @@
       else raise TERM ("dest_bin " ^ c, [tm])
   | dest_bin c _ tm = raise TERM ("dest_bin " ^ c, [tm]);
 
-
 end;