diff -r 0755f8fd56b3 -r 71225f4a4635 Quot/quotient_typ.ML
--- a/Quot/quotient_typ.ML	Thu Dec 31 23:53:10 2009 +0100
+++ b/Quot/quotient_typ.ML	Fri Jan 01 01:08:19 2010 +0100
@@ -217,9 +217,15 @@
 (* - its mixfix annotation                                  *)
 (* - the type to be quotient                                *)
 (* - the relation according to which the type is quotient   *)
+(*                                                          *)
+(* opens a proof-state in which one has to show that the    *)
+(* relation is an equivalence relation                      *)
 
 fun quotient_type quot_list lthy = 
 let
+  (* sanity check *)  
+  val _ = map sanity_check quot_list 
+
   fun mk_goal (rty, rel) =
   let
     val equivp_ty = ([rty, rty] ---> @{typ bool}) --> @{typ bool}
@@ -231,14 +237,11 @@
               
   fun after_qed thms lthy =
     fold_map mk_typedef_main (quot_list ~~ thms) lthy |> snd
-
-  (* sanity check *)  
-  val _ = map sanity_check quot_list 
 in
   theorem after_qed goals lthy
 end
            
-fun quotient_type_cmd spec lthy = 
+fun quotient_type_cmd specs lthy = 
 let
   fun parse_spec ((((vs, qty_name), mx), rty_str), rel_str) =
   let
@@ -248,7 +251,7 @@
     ((vs, qty_name, mx), (rty, rel))
   end
 in
-  quotient_type (map parse_spec spec) lthy
+  quotient_type (map parse_spec specs) lthy
 end
 
 val quotspec_parser =