--- a/Quot/quotient_typ.ML	Fri Dec 25 00:58:06 2009 +0100
+++ b/Quot/quotient_typ.ML	Sat Dec 26 07:15:30 2009 +0100
@@ -39,6 +39,7 @@
 end
 
 
+(********************************)
 (* definition of quotient types *)
 (********************************)
 
@@ -52,11 +53,11 @@
                |> Variable.variant_frees lthy [rel]
                |> map Free
 in
-  lambda c
-    (HOLogic.exists_const rty $
-       lambda x (HOLogic.mk_eq (c, (rel $ x))))
+  lambda c (HOLogic.exists_const rty $
+     lambda x (HOLogic.mk_eq (c, (rel $ x))))
 end
 
+
 (* makes the new type definitions and proves non-emptyness *)
 fun typedef_make (vs, qty_name, mx, rel, rty) lthy =
 let
@@ -69,10 +70,11 @@
   Local_Theory.theory_result
     (Typedef.add_typedef false NONE
        (qty_name, vs, mx)
-         (typedef_term rel rty lthy)
-           NONE typedef_tac) lthy
+          (typedef_term rel rty lthy)
+             NONE typedef_tac) lthy
 end
 
+
 (* tactic to prove the Quot_Type theorem for the new type *)
 fun typedef_quot_type_tac equiv_thm (typedef_info: Typedef.info) =
 let
@@ -89,6 +91,7 @@
           rtac rep_inj]) 1
 end
 
+
 (* proves the Quot_Type theorem *)
 fun typedef_quot_type_thm (rel, abs, rep, equiv_thm, typedef_info) lthy =
 let
@@ -116,6 +119,7 @@
     (K typedef_quotient_thm_tac)
 end
 
+
 (* main function for constructing a quotient type *)
 fun mk_typedef_main (((vs, qty_name, mx), (rty, rel)), equiv_thm) lthy =
 let
@@ -164,6 +168,7 @@
   ||>> note (equiv_thm_name, equiv_thm, [intern_attr equiv_rules_add])
 end
 
+
 (* sanity checks of the quotient type specifications *)
 fun sanity_check ((vs, qty_name, _), (rty, rel)) =
 let
@@ -203,7 +208,10 @@
   if null errs then () else error (cat_lines errs)
 end
 
+
+(******************************)
 (* interface and syntax setup *)
+(******************************)
 
 (* the ML-interface takes a list of 5-tuples consisting of  *)
 (*                                                          *)