diff -r fd718dde1d61 -r 57944c1ef728 Quot/QuotMain.thy
--- a/Quot/QuotMain.thy	Thu Dec 10 11:19:34 2009 +0100
+++ b/Quot/QuotMain.thy	Thu Dec 10 12:25:12 2009 +0100
@@ -435,6 +435,15 @@
 (* 5. then simplification like 0 *)
 (* finally jump back to 1 *)
 
+ML {*
+fun quotient_tac ctxt =
+  REPEAT_ALL_NEW (FIRST'
+    [rtac @{thm identity_quotient},
+     resolve_tac (quotient_rules_get ctxt)])
+
+fun quotient_solver_tac ss = quotient_tac (Simplifier.the_context ss)
+val quotient_solver = Simplifier.mk_solver' "Quotient goal solver" quotient_solver_tac
+*}
 
 ML {*
 fun regularize_tac ctxt =
@@ -444,8 +453,8 @@
   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 babs_reg_eqv}
-                       addsimprocs [simproc] addSolver equiv_solver
+                       addsimps @{thms ball_reg_eqv bex_reg_eqv babs_reg_eqv babs_simp}
+                       addsimprocs [simproc] addSolver equiv_solver addSolver quotient_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 (OF1 @{thm eq_imp_rel}) (equiv_rules_get ctxt)
@@ -549,16 +558,6 @@
 section {* Injection Tactic *}
 
 ML {*
-fun quotient_tac ctxt =
-  REPEAT_ALL_NEW (FIRST'
-    [rtac @{thm identity_quotient},
-     resolve_tac (quotient_rules_get ctxt)])
-
-fun quotient_solver_tac ss = quotient_tac (Simplifier.the_context ss)
-val quotient_solver = Simplifier.mk_solver' "Quotient goal solver" quotient_solver_tac
-*}
-
-ML {*
 fun solve_quotient_assums ctxt thm =
 let 
   val goal = hd (Drule.strip_imp_prems (cprop_of thm)) 
@@ -619,6 +618,9 @@
 lemma QUOT_TRUE_imp: "QUOT_TRUE a \<equiv> QUOT_TRUE b"
 by (simp add: QUOT_TRUE_def)
 
+lemma regularize_to_injection: "(QUOT_TRUE l \<Longrightarrow> y) \<Longrightarrow> (l = r) \<longrightarrow> y"
+  by(auto simp add: QUOT_TRUE_def)
+
 ML {*
 fun quot_true_conv1 ctxt fnctn ctrm =
   case (term_of ctrm) of