diff -r 116c7a30e0a2 -r a32f4f866051 Quot/quotient_typ.ML
--- a/Quot/quotient_typ.ML	Mon Jan 11 15:58:38 2010 +0100
+++ b/Quot/quotient_typ.ML	Mon Jan 11 16:33:00 2010 +0100
@@ -39,9 +39,8 @@
 end
 
 
-(********************************)
-(* definition of quotient types *)
-(********************************)
+
+(*** definition of quotient types ***)
 
 val mem_def1 = @{lemma "y : S ==> S y" by (simp add: mem_def)}
 val mem_def2 = @{lemma "S y ==> y : S" by (simp add: mem_def)}
@@ -224,26 +223,27 @@
 end
 
 
-(******************************)
-(* interface and syntax setup *)
-(******************************)
+
+(*** interface and syntax setup ***)
+
 
-(* the ML-interface takes a list of 5-tuples consisting of  *)
-(*                                                          *)
-(* - the name of the quotient type                          *)
-(* - its free type variables (first argument)               *)
-(* - its mixfix annotation                                  *)
-(* - the type to be quotient                                *)
-(* - the relation according to which the type is quotient   *)
-(*                                                          *)
-(* it opens a proof-state in which one has to show that the *)
-(* relations are equivalence relations                      *)
+(* the ML-interface takes a list of 5-tuples consisting of 
+                                                         
+    - the name of the quotient type                       
+    - its free type variables (first argument)            
+    - its mixfix annotation                               
+    - the type to be quotient                             
+    - the relation according to which the type is quotient  
+                                                        
+   it opens a proof-state in which one has to show that the
+   relations are equivalence relations                      
+*)
 
 fun quotient_type quot_list lthy = 
 let
   (* sanity check *)  
-  val _ = map sanity_check quot_list 
-  val _ = map (map_check lthy) quot_list
+  val _ = List.app sanity_check quot_list 
+  val _ = List.app (map_check lthy) quot_list
 
   fun mk_goal (rty, rel) =
   let