diff -r 9c6991411e1f -r a68c51dd85b3 QuotMain.thy
--- a/QuotMain.thy	Sun Dec 06 02:41:35 2009 +0100
+++ b/QuotMain.thy	Sun Dec 06 04:03:08 2009 +0100
@@ -1051,27 +1051,28 @@
   in (f, Abs ("x", T, mk_abs 0 g)) end;
 *}
 
-thm lambda_prs
-
 ML {*
 fun lambda_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 fun_map}, _) $ r1 $ a2) $ (Abs _)) =>
+     let
+       val thy = ProofContext.theory_of ctxt
+       val (ty_b, ty_a) = dest_fun_type (fastype_of r1)
+       val (ty_c, ty_d) = dest_fun_type (fastype_of a2)
+       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
+        (*val _ = tracing "lambda_prs"
+          val _ = tracing ("redex:\n" ^ (Syntax.string_of_term ctxt (term_of ctrm)))
+          val _ = tracing ("instantiated rule:\n" ^ (Syntax.string_of_term ctxt (prop_of ti)))*)
+     in
+       Conv.rewr_conv ti ctrm
+     end
   | _ => Conv.all_conv ctrm
 *}
 
@@ -1083,29 +1084,27 @@
 *}
 
 (*
- Cleaning the theorem consists of 6 kinds of rewrites.
+ Cleaning the theorem consists of three rewriting steps.
  The first two need to be done before fun_map is unfolded
 
- - lambda_prs:
+ 1) lambda_prs:
      (Rep1 ---> Abs2) (\<lambda>x. Rep2 (f (Abs1 x)))  ---->  f
 
- - all_prs (and the same for exists: ex_prs)
-     \<forall>x\<in>Respects R. (abs ---> id) f  ---->  \<forall>x. f
+    Implemented as conversion since it is not a pattern.
 
- - Rewriting with definitions from the argument defs
-     NewConst  ---->  (rep ---> abs) oldConst
+ 2) all_prs (the same for exists):
+     Ball (Respects R) ((abs ---> id) f)  ---->  All f
 
- - Quotient_rel_rep:
-     Rel (Rep x) (Rep y)  ---->  x = y
+    Rewriting with definitions from the argument defs
+     (rep ---> abs) oldConst ----> newconst
 
- - ABS_REP
-     Abs (Rep x)  ---->  x
+ 3) Quotient_rel_rep:
+      Rel (Rep x) (Rep y)  ---->  x = y
 
- - id_simps; fun_map.simps
+    Quotient_abs_rep:
+      Abs (Rep x)  ---->  x
 
- The first one is implemented as a conversion (fast).
- The second one is an EqSubst (slow).
- The rest are a simp_tac and are fast.
+    id_simps; fun_map.simps
 *)
 
 ML {*
@@ -1113,28 +1112,17 @@
   let
     val thy = ProofContext.theory_of lthy;
     val defs = map (Thm.varifyT o symmetric o #def) (qconsts_dest thy)
+      (* FIXME: shouldn't the definitions already be varified? *)
     val thms1 = @{thms all_prs ex_prs} @ defs
     val thms2 = @{thms eq_reflection[OF fun_map.simps]} 
                 @ @{thms id_simps Quotient_abs_rep Quotient_rel_rep} 
-    fun simp_ctxt thms = HOL_basic_ss addsimps thms addSolver quotient_solver
-    (* FIXME: use of someting smaller than HOL_basic_ss *)
+    fun simps 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 "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" (simp_tac (simp_ctxt thms2)),
-
-      (* final step *)
-      NDT lthy "d" (TRY o rtac refl)
-    ]
+    EVERY' [lambda_prs_tac lthy,
+            simp_tac (simps thms1),
+            simp_tac (simps thms2),
+            TRY o rtac refl]
   end
 *}