--- a/IntEx.thy	Sat Dec 05 22:16:17 2009 +0100
+++ b/IntEx.thy	Sat Dec 05 22:38:42 2009 +0100
@@ -154,10 +154,12 @@
 abbreviation 
   "Resp \<equiv> Respects"
 
+
 lemma "PLUS a b = PLUS a b"
 apply(tactic {* procedure_tac @{context} @{thm test1} 1 *})
 apply(tactic {* regularize_tac @{context} [rel_eqv] 1 *})
 apply(tactic {* all_inj_repabs_tac_intex @{context} 1*})
+apply(tactic {* simp_tac (HOL_basic_ss addSolver quotient_solver addsimps @{thms all_prs})  1 *})
 apply(tactic {* clean_tac @{context} 1 *}) 
 done
 

--- a/QuotMain.thy	Sat Dec 05 22:16:17 2009 +0100
+++ b/QuotMain.thy	Sat Dec 05 22:38:42 2009 +0100
@@ -1044,54 +1044,28 @@
 fun lambda_allex_prs_simple_conv ctxt ctrm =
   case (term_of ctrm) of
     ((Const (@{const_name fun_map}, _) $ r1 $ a2) $ (Abs _)) =>
-  let
-    val (ty_b, ty_a) = dest_fun_type (fastype_of r1);
-    val (ty_c, ty_d) = dest_fun_type (fastype_of a2);
-    val thy = ProofContext.theory_of ctxt;
-    val tyinst = map (SOME o (ctyp_of thy)) [ty_a, ty_b, ty_c, ty_d]
-    val tinst = [NONE, NONE, SOME (cterm_of thy r1), NONE, SOME (cterm_of thy a2)]
-    val lpi = Drule.instantiate' tyinst tinst @{thm lambda_prs};
-    val te = @{thm eq_reflection} OF [solve_quotient_assums ctxt (solve_quotient_assums ctxt lpi)]
-    val ts = MetaSimplifier.rewrite_rule @{thms id_simps} te
-    val tl = Thm.lhs_of ts;
-    val (insp, inst) = make_inst (term_of tl) (term_of ctrm);
-    val ti = Drule.instantiate ([], [(cterm_of thy insp, cterm_of thy inst)]) ts;
-  in
-    Conv.rewr_conv ti ctrm
-  end
-  | (Const (@{const_name Ball}, _) $ (Const (@{const_name Respects}, _) $ R) $
-    (((Const (@{const_name fun_map}, _) $ absf $ (Const (@{const_name id}, _)))) $ f)) =>
-  let
-    val (ty_a, ty_b) = dest_fun_type (fastype_of absf);
-    val thy = ProofContext.theory_of ctxt;
-    val tyinst = map (SOME o (ctyp_of thy)) [ty_a, ty_b];
-    val tinst = [SOME (cterm_of thy R), SOME (cterm_of thy absf), NONE, SOME (cterm_of thy f)];
-    val thm = Drule.instantiate' tyinst tinst @{thm all_prs};
-    val ti = @{thm eq_reflection} OF [solve_quotient_assums ctxt thm];
-  in
-    Conv.rewr_conv ti ctrm
-  end
-  | (Const (@{const_name Bex}, _) $ (Const (@{const_name Respects}, _) $ R) $
-    (((Const (@{const_name fun_map}, _) $ absf $ (Const (@{const_name id}, _)))) $ f)) =>
-  let
-    val (ty_a, ty_b) = dest_fun_type (fastype_of absf);
-    val thy = ProofContext.theory_of ctxt;
-    val tyinst = map (SOME o (ctyp_of thy)) [ty_a, ty_b];
-    val tinst = [SOME (cterm_of thy R), SOME (cterm_of thy absf), NONE, SOME (cterm_of thy f)];
-    val thm = Drule.instantiate' tyinst tinst @{thm ex_prs};
-    val ti = @{thm eq_reflection} OF [solve_quotient_assums ctxt thm];
-  in
-    Conv.rewr_conv ti ctrm
-  end
+    let
+      val (ty_b, ty_a) = dest_fun_type (fastype_of r1);
+      val (ty_c, ty_d) = dest_fun_type (fastype_of a2);
+      val thy = ProofContext.theory_of ctxt;
+      val tyinst = map (SOME o (ctyp_of thy)) [ty_a, ty_b, ty_c, ty_d]
+      val tinst = [NONE, NONE, SOME (cterm_of thy r1), NONE, SOME (cterm_of thy a2)]
+      val lpi = Drule.instantiate' tyinst tinst @{thm lambda_prs};
+      val te = @{thm eq_reflection} OF [solve_quotient_assums ctxt (solve_quotient_assums ctxt lpi)]
+      val ts = MetaSimplifier.rewrite_rule @{thms id_simps} te
+      val tl = Thm.lhs_of ts;
+      val (insp, inst) = make_inst (term_of tl) (term_of ctrm);
+      val ti = Drule.instantiate ([], [(cterm_of thy insp, cterm_of thy inst)]) ts;
+    in
+      Conv.rewr_conv ti ctrm
+    end
   | _ => Conv.all_conv ctrm
 *}
 
 ML {*
 val lambda_allex_prs_conv =
   More_Conv.top_conv lambda_allex_prs_simple_conv
-*}
 
-ML {*
 fun lambda_allex_prs_tac ctxt = CONVERSION (lambda_allex_prs_conv ctxt)
 *}
 
@@ -1121,7 +1095,6 @@
  The rest are a simp_tac and are fast.
 *)
 
-ML {* fun OF1 thm1 thm2 = thm2 RS thm1 *}
 ML {*
 fun quotient_solver_tac ss = quotient_tac (Simplifier.the_context ss)
 val quotient_solver = Simplifier.mk_solver' "Quotient goal solver" quotient_solver_tac
@@ -1132,21 +1105,25 @@
   let
     val thy = ProofContext.theory_of lthy;
     val defs = map (Thm.varifyT o #def) (qconsts_dest thy)
-    val thms = @{thms eq_reflection[OF fun_map.simps]} 
-               @ @{thms id_simps Quotient_abs_rep Quotient_rel_rep} 
-               @ defs
-    val simp_ctxt = HOL_basic_ss addsimps thms addSolver quotient_solver
+    val thms1 = @{thms all_prs ex_prs}
+    val thms2 = @{thms eq_reflection[OF fun_map.simps]} 
+                @ @{thms id_simps Quotient_abs_rep Quotient_rel_rep} 
+                @ defs
+    fun simp_ctxt thms = HOL_basic_ss addsimps thms addSolver quotient_solver
+    (* FIXME: use of someting smaller than HOL_basic_ss *)
   in
     EVERY' [
       (* (rep1 ---> abs2) (\<lambda>x. rep2 (f (abs1 x)))  ---->  f *)
+      NDT lthy "a" (TRY o lambda_allex_prs_tac lthy),
+
       (* Ball (Respects R) ((abs ---> id) f)  ---->  All f *)
-      NDT lthy "a" (TRY o lambda_allex_prs_tac lthy),
+      NDT lthy "b" (simp_tac (simp_ctxt thms1)),
 
       (* NewConst  ----->  (rep ---> abs) oldConst *)
       (* abs (rep x)  ----->  x                    *)
       (* R (Rep x) (Rep y) -----> x = y            *)
       (* id_simps; fun_map.simps                   *)
-      NDT lthy "c" (TRY o simp_tac simp_ctxt),
+      NDT lthy "c" (simp_tac (simp_ctxt thms2)),
 
       (* final step *)
       NDT lthy "d" (TRY o rtac refl)
@@ -1225,11 +1202,11 @@
   val reg_goal = 
         Syntax.check_term ctxt (regularize_trm ctxt rtrm' qtrm')
         handle (LIFT_MATCH s) => lift_match_error ctxt s rtrm qtrm
-  val _ = tracing "Regularization done."
+  val _ = warning "Regularization done."
   val inj_goal = 
         Syntax.check_term ctxt (inj_repabs_trm ctxt (reg_goal, qtrm'))
         handle (LIFT_MATCH s) => lift_match_error ctxt s rtrm qtrm
-  val _ = tracing "RepAbs Injection done."
+  val _ = warning "RepAbs Injection done."
 in
   Drule.instantiate' []
     [SOME (cterm_of thy rtrm'),