--- a/Quot/quotient_typ.ML	Tue Feb 09 15:43:39 2010 +0100
+++ b/Quot/quotient_typ.ML	Tue Feb 09 15:55:58 2010 +0100
@@ -55,9 +55,10 @@
 (* constructs the term lambda (c::rty => bool). EX (x::rty). c = rel x *)
 fun typedef_term rel rty lthy =
 let
-  val [x, c] = [("x", rty), ("c", HOLogic.mk_setT rty)]
-               |> Variable.variant_frees lthy [rel]
-               |> map Free
+  val [x, c] =
+    [("x", rty), ("c", HOLogic.mk_setT rty)]
+    |> Variable.variant_frees lthy [rel]
+    |> map Free
 in
   lambda c (HOLogic.exists_const rty $
      lambda x (HOLogic.mk_eq (c, (rel $ x))))
@@ -86,12 +87,12 @@
   val abs_inv = mem_def2 RS #Abs_inverse typedef_info
   val rep_inj = #Rep_inject typedef_info
 in
-  (rtac @{thm Quot_Type.intro} THEN' 
-   RANGE [rtac equiv_thm,
-          rtac rep_thm,
-          rtac rep_inv,
-          EVERY' (map rtac [abs_inv, @{thm exI}, @{thm refl}]),
-          rtac rep_inj]) 1
+  (rtac @{thm Quot_Type.intro} THEN' RANGE [
+    rtac equiv_thm,
+    rtac rep_thm,
+    rtac rep_inv,
+    EVERY' (map rtac [abs_inv, @{thm exI}, @{thm refl}]),
+    rtac rep_inj]) 1
 end
 
 
@@ -99,8 +100,9 @@
 fun typedef_quot_type_thm (rel, abs, rep, equiv_thm, typedef_info) lthy =
 let
   val quot_type_const = Const (@{const_name "Quot_Type"}, dummyT)
-  val goal = HOLogic.mk_Trueprop (quot_type_const $ rel $ abs $ rep)
-             |> Syntax.check_term lthy
+  val goal =
+    HOLogic.mk_Trueprop (quot_type_const $ rel $ abs $ rep)
+    |> Syntax.check_term lthy
 in
   Goal.prove lthy [] [] goal
     (K (typedef_quot_type_tac equiv_thm typedef_info))
@@ -110,13 +112,15 @@
 fun typedef_quotient_thm (rel, abs, rep, abs_def, rep_def, quot_type_thm) lthy =
 let
   val quotient_const = Const (@{const_name "Quotient"}, dummyT)
-  val goal = HOLogic.mk_Trueprop (quotient_const $ rel $ abs $ rep)
-             |> Syntax.check_term lthy
+  val goal =
+    HOLogic.mk_Trueprop (quotient_const $ rel $ abs $ rep)
+    |> Syntax.check_term lthy
 
   val typedef_quotient_thm_tac =
-    EVERY1 [K (rewrite_goals_tac [abs_def, rep_def]),
-            rtac @{thm Quot_Type.Quotient},
-            rtac quot_type_thm]
+    EVERY1 [
+      K (rewrite_goals_tac [abs_def, rep_def]),
+      rtac @{thm Quot_Type.Quotient},
+      rtac quot_type_thm]
 in
   Goal.prove lthy [] [] goal
     (K typedef_quotient_thm_tac)
@@ -161,10 +165,10 @@
   (* storing the quot-info *)
   (* FIXME: VarifyT should not be used - at the moment it allows matching against the types. *)
   fun qinfo phi = transform_quotdata phi
-                    {qtyp = Logic.varifyT Abs_ty, rtyp = Logic.varifyT rty, 
-                     equiv_rel = map_types Logic.varifyT rel, equiv_thm = equiv_thm}
+    {qtyp = Logic.varifyT Abs_ty, rtyp = Logic.varifyT rty,
+     equiv_rel = map_types Logic.varifyT rel, equiv_thm = equiv_thm}
   val lthy4 = Local_Theory.declaration true
-                (fn phi => quotdata_update_gen qty_full_name (qinfo phi)) lthy3  
+    (fn phi => quotdata_update_gen qty_full_name (qinfo phi)) lthy3
 in
   lthy4
   |> note (quotient_thm_name, quotient_thm, [intern_attr quotient_rules_add])
@@ -224,9 +228,9 @@
 
   val warns = map_check_aux rty []
 in
-  if null warns then () 
+  if null warns then ()
   else warning ("No map function defined for " ^ commas warns ^
-                ". This will cause problems later on.")
+    ". This will cause problems later on.")
 end