--- a/Quot/quotient_typ.ML	Sat Dec 26 08:06:45 2009 +0100
+++ b/Quot/quotient_typ.ML	Sat Dec 26 09:03:35 2009 +0100
@@ -62,10 +62,7 @@
 fun typedef_make (vs, qty_name, mx, rel, rty) lthy =
 let
   val typedef_tac =
-     EVERY1 [rtac @{thm exI},
-             rtac mem_def2, 
-             rtac @{thm exI},
-             rtac @{thm refl}]
+     EVERY1 (map rtac [@{thm exI}, mem_def2, @{thm exI}, @{thm refl}])
 in
   Local_Theory.theory_result
     (Typedef.add_typedef false NONE
@@ -87,7 +84,7 @@
    RANGE [rtac equiv_thm,
           rtac rep_thm,
           rtac rep_inv,
-          EVERY' [rtac abs_inv, rtac @{thm exI}, rtac @{thm refl}],
+          EVERY' (map rtac [abs_inv, @{thm exI}, @{thm refl}]),
           rtac rep_inj]) 1
 end
 
@@ -134,7 +131,7 @@
   val Abs_const = Const (Abs_name, Rep_ty --> Abs_ty)
   val Rep_const = Const (Rep_name, Abs_ty --> Rep_ty)
 
-  (* more abstract abs and rep definitions *)
+  (* more useful abs and rep definitions *)
   val abs_const = Const (@{const_name "Quot_Type.abs"}, dummyT )
   val rep_const = Const (@{const_name "Quot_Type.rep"}, dummyT )
   val abs_trm = Syntax.check_term lthy1 (abs_const $ rel $ Abs_const)