--- a/FSet.thy	Fri Nov 27 10:04:49 2009 +0100
+++ b/FSet.thy	Fri Nov 27 13:59:52 2009 +0100
@@ -347,10 +347,14 @@
 apply(tactic {* procedure_tac @{context} @{thm list.induct} 1 *})
 apply(tactic {* regularize_tac @{context} [rel_eqv] [rel_refl] 1 *})
 prefer 2
-apply (tactic {* clean_tac @{context} [quot] defs [(@{typ "('a list \<Rightarrow> bool)"},@{typ "('a fset \<Rightarrow> bool)"})] 1 *})
+apply (tactic {* clean_tac @{context} [quot] defs 
+                 [(@{typ "('a list \<Rightarrow> bool)"},@{typ "('a fset \<Rightarrow> bool)"})] 1 *})
 apply(tactic {* r_mk_comb_tac' @{context} rty [quot] rel_refl trans2 rsp_thms 1*})
 done
 
+
+
+
 quotient_def
   fset_rec::"'a \<Rightarrow> ('b \<Rightarrow> 'b fset \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> 'b fset \<Rightarrow> 'a"
 where

--- a/QuotMain.thy	Fri Nov 27 10:04:49 2009 +0100
+++ b/QuotMain.thy	Fri Nov 27 13:59:52 2009 +0100
@@ -505,7 +505,7 @@
   (ObjectLogic.full_atomize_tac) THEN'
   REPEAT_ALL_NEW (FIRST'
    [(K (print_tac "start")) THEN' (K no_tac),
-    DT ctxt "1" (FIRST' (map rtac rel_refl)),
+    DT ctxt "1" (resolve_tac rel_refl),
     DT ctxt "2" atac,
     DT ctxt "3" (rtac @{thm universal_twice}),
     DT ctxt "4" (rtac @{thm impI} THEN' atac),
@@ -514,7 +514,7 @@
       [(@{thm equiv_res_forall} OF [rel_eqv]),
        (@{thm equiv_res_exists} OF [rel_eqv])]),
     (* For a = b \<longrightarrow> a \<approx> b *)
-    DT ctxt "7" (rtac @{thm impI} THEN' (asm_full_simp_tac HOL_ss) THEN' (FIRST' (map rtac rel_refl))),
+    DT ctxt "7" (rtac @{thm impI} THEN' (asm_full_simp_tac HOL_ss) THEN' (resolve_tac rel_refl)),
     DT ctxt "8" (rtac @{thm RIGHT_RES_FORALL_REGULAR})
   ]);
 *}
@@ -572,11 +572,10 @@
 (* FIXME: OPTION_EQUIV, PAIR_EQUIV, ... *)
 ML {*
 fun equiv_tac rel_eqvs =
-  REPEAT_ALL_NEW(FIRST' [
-    FIRST' (map rtac rel_eqvs),
-    rtac @{thm IDENTITY_EQUIV},
-    rtac @{thm LIST_EQUIV}
-  ])
+  REPEAT_ALL_NEW (FIRST' 
+    [resolve_tac rel_eqvs,
+     rtac @{thm IDENTITY_EQUIV},
+     rtac @{thm LIST_EQUIV}])
 *}
 
 ML {*
@@ -593,16 +592,15 @@
   (ObjectLogic.full_atomize_tac) THEN'
   (simp_tac ((Simplifier.context ctxt empty_ss) addsimps subs))
   THEN'
-  REPEAT_ALL_NEW (FIRST' [
-    (rtac @{thm RIGHT_RES_FORALL_REGULAR}),
-    (rtac @{thm LEFT_RES_EXISTS_REGULAR}),
-    (resolve_tac (Inductive.get_monos ctxt)),
-    (rtac @{thm ball_respects_refl} THEN' (RANGE [SOLVES' (equiv_tac rel_eqvs)])),
-    (rtac @{thm bex_respects_refl} THEN' (RANGE [SOLVES' (equiv_tac rel_eqvs)])),
-    rtac @{thm move_forall},
-    rtac @{thm move_exists},
-    (rtac @{thm impI} THEN' (asm_full_simp_tac HOL_ss) THEN' FIRST' (map rtac rel_refl))
-  ])
+  REPEAT_ALL_NEW (FIRST' 
+    [(rtac @{thm RIGHT_RES_FORALL_REGULAR}),
+     (rtac @{thm LEFT_RES_EXISTS_REGULAR}),
+     (resolve_tac (Inductive.get_monos ctxt)),
+     (rtac @{thm ball_respects_refl} THEN' (RANGE [SOLVES' (equiv_tac rel_eqvs)])),
+     (rtac @{thm bex_respects_refl} THEN' (RANGE [SOLVES' (equiv_tac rel_eqvs)])),
+     rtac @{thm move_forall},
+     rtac @{thm move_exists},
+     (rtac @{thm impI} THEN' (asm_full_simp_tac HOL_ss) THEN' (resolve_tac rel_refl))])
   end
 *}
 
@@ -732,14 +730,13 @@
 
 ML {*
 fun quotient_tac quot_thms =
-  REPEAT_ALL_NEW (FIRST' [
-    rtac @{thm FUN_QUOTIENT},
-    FIRST' (map rtac quot_thms),
-    rtac @{thm IDENTITY_QUOTIENT},
-    (* For functional identity quotients, (op = ---> op =) *)
-    (* TODO: think about the other way around, if we need to shorten the relation *)
-    CHANGED o (simp_tac (HOL_ss addsimps @{thms id_simps}))
-  ])
+  REPEAT_ALL_NEW (FIRST' 
+    [rtac @{thm FUN_QUOTIENT},
+     resolve_tac quot_thms,
+     rtac @{thm IDENTITY_QUOTIENT},
+     (* For functional identity quotients, (op = ---> op =) *)
+     (* TODO: think about the other way around, if we need to shorten the relation *)
+     CHANGED o (simp_tac (HOL_ss addsimps @{thms id_simps}))])
 *}
 
 ML {*
@@ -817,21 +814,21 @@
 ML {*
 fun r_mk_comb_tac ctxt rty quot_thms rel_refl trans2 rsp_thms =
   (FIRST' [
-    FIRST' (map rtac trans2),
+    resolve_tac trans2,
     LAMBDA_RES_TAC ctxt,
     rtac @{thm RES_FORALL_RSP},
     ball_rsp_tac ctxt,
     rtac @{thm RES_EXISTS_RSP},
     bex_rsp_tac ctxt,
-    FIRST' (map rtac rsp_thms),
-    rtac refl,
+    resolve_tac rsp_thms,
+    rtac @{thm refl},
     (instantiate_tac @{thm REP_ABS_RSP(1)} ctxt THEN' 
          (RANGE [SOLVES' (quotient_tac quot_thms)])),
     (APPLY_RSP_TAC rty ctxt THEN' 
          (RANGE [SOLVES' (quotient_tac quot_thms), SOLVES' (quotient_tac quot_thms)])),
     Cong_Tac.cong_tac @{thm cong},
     rtac @{thm ext},
-    FIRST' (map rtac rel_refl),
+    resolve_tac rel_refl,
     atac,
     SOLVES' (simp_tac (HOL_ss addsimps @{thms FUN_REL.simps})),
     WEAK_LAMBDA_RES_TAC ctxt,
@@ -863,24 +860,24 @@
 *)
 
 ML {*
-fun r_mk_comb_tac' ctxt rty quot_thms reflex_thm trans_thm rsp_thms =
+fun r_mk_comb_tac' ctxt rty quot_thms rel_refl trans2 rsp_thms =
   REPEAT_ALL_NEW (FIRST' [
     (K (print_tac "start")) THEN' (K no_tac), 
-    DT ctxt "1" (rtac trans_thm),
+    DT ctxt "1" (resolve_tac trans2),
     DT ctxt "2" (LAMBDA_RES_TAC ctxt),
     DT ctxt "3" (rtac @{thm RES_FORALL_RSP}),
     DT ctxt "4" (ball_rsp_tac ctxt),
     DT ctxt "5" (rtac @{thm RES_EXISTS_RSP}),
     DT ctxt "6" (bex_rsp_tac ctxt),
-    DT ctxt "7" (FIRST' (map rtac rsp_thms)),
-    DT ctxt "8" (rtac refl),
+    DT ctxt "7" (resolve_tac rsp_thms),
+    DT ctxt "8" (rtac @{thm refl}),
     DT ctxt "9" ((instantiate_tac @{thm REP_ABS_RSP(1)} ctxt 
                   THEN' (RANGE [SOLVES' (quotient_tac quot_thms)]))),
     DT ctxt "A" ((APPLY_RSP_TAC rty ctxt THEN' 
                 (RANGE [SOLVES' (quotient_tac quot_thms), SOLVES' (quotient_tac quot_thms)]))),
     DT ctxt "B" (Cong_Tac.cong_tac @{thm cong}),
     DT ctxt "C" (rtac @{thm ext}),
-    DT ctxt "D" (rtac reflex_thm),
+    DT ctxt "D" (resolve_tac rel_refl),
     DT ctxt "E" (atac),
     DT ctxt "F" (SOLVES' (simp_tac (HOL_ss addsimps @{thms FUN_REL.simps}))),
     DT ctxt "G" (WEAK_LAMBDA_RES_TAC ctxt),
@@ -938,7 +935,7 @@
 ML {*
 fun allex_prs_tac lthy quot =
   (EqSubst.eqsubst_tac lthy [0] @{thms FORALL_PRS[symmetric] EXISTS_PRS[symmetric]})
-  THEN' (quotient_tac quot);
+  THEN' (quotient_tac quot)
 *}
 
 ML {*