diff -r 0cf166548856 -r 120e479ed367 Quot/QuotMain.thy
--- a/Quot/QuotMain.thy	Mon Dec 07 15:21:51 2009 +0100
+++ b/Quot/QuotMain.thy	Mon Dec 07 17:57:33 2009 +0100
@@ -183,6 +183,11 @@
     setmksimps (mksimps [])
 *}
 
+ML {*
+(* TODO/FIXME not needed anymore? *)
+fun SOLVES' tac = tac THEN_ALL_NEW (fn _ => no_tac)
+*}
+
 section {* atomize *}
 
 lemma atomize_eqv[atomize]:
@@ -486,8 +491,8 @@
 
 ML {*
 fun equiv_tac ctxt =
-  REPEAT_ALL_NEW (FIRST' 
-    [resolve_tac (equiv_rules_get ctxt)])
+  (K (print_tac "equiv tac")) THEN'
+  REPEAT_ALL_NEW (resolve_tac (equiv_rules_get ctxt))
 *}
 
 ML {*
@@ -577,20 +582,23 @@
   val pat_bex  = @{term "Bex (Respects (R1 ===> R2)) P"}
   val simproc = Simplifier.simproc_i thy "" [pat_ball, pat_bex] (K (ball_bex_range_simproc))
   val simpset = (mk_minimal_ss ctxt) 
-                       addsimps @{thms ball_reg_eqv bex_reg_eqv}
+                       addsimps @{thms ball_reg_eqv bex_reg_eqv babs_reg_eqv}
                        addsimprocs [simproc] addSolver equiv_solver
   (* TODO: Make sure that there are no list_rel, pair_rel etc involved *)
+  (* can this cause loops in equiv_tac ? *)
   val eq_eqvs = map (fn x => @{thm eq_imp_rel} OF [x]) (equiv_rules_get ctxt)
 in
   ObjectLogic.full_atomize_tac THEN'
   simp_tac simpset THEN'
-  REPEAT_ALL_NEW (FIRST' [
+  REPEAT_ALL_NEW (CHANGED o FIRST' [
     rtac @{thm ball_reg_right},
     rtac @{thm bex_reg_left},
     resolve_tac (Inductive.get_monos ctxt),
     rtac @{thm ball_all_comm},
     rtac @{thm bex_ex_comm},
-    resolve_tac eq_eqvs,
+    resolve_tac eq_eqvs,  
+    (* should be equivalent to the above, but causes loops: *) 
+    (* rtac @{thm eq_imp_rel} THEN' SOLVES' (equiv_tac ctxt), *)
     simp_tac simpset])
 end
 *}
@@ -848,9 +856,6 @@
         handle ERROR "find_qt_asm: no pair" => no_tac)
     | _ => no_tac)
 *}
-ML {*
-fun SOLVES' tac = tac THEN_ALL_NEW (fn _ => no_tac)
-*}
 
 ML {*
 fun rep_abs_rsp_tac ctxt =