--- a/QuotMain.thy	Wed Dec 02 23:31:30 2009 +0100
+++ b/QuotMain.thy	Thu Dec 03 02:18:21 2009 +0100
@@ -1083,8 +1083,10 @@
       | Bound j => if i = j then error "make_inst" else t
       | _ => t);
   in (f, Abs ("x", T, mk_abs 0 g)) end;
+*}
 
-fun lambda_prs_conv1 ctxt quot_thms ctrm =
+ML {*
+fun lambda_prs_simple_conv quot_thms ctxt ctrm =
   case (term_of ctrm) of ((Const (@{const_name "fun_map"}, _) $ r1 $ a2) $ (Abs _)) =>
   let
     val (_, [ty_b, ty_a]) = dest_Type (fastype_of r1);
@@ -1108,27 +1110,21 @@
   in
     Conv.rewr_conv ti ctrm
   end
+  | _ => Conv.all_conv ctrm
 *}
 
 (* quot stands for the QUOTIENT theorems: *)
 (* could be potentially all of them       *)
 ML {*
-fun lambda_prs_conv ctxt quot ctrm =
-  case (term_of ctrm) of
-    (Const (@{const_name "fun_map"}, _) $ _ $ _) $ (Abs _) =>
-      (Conv.arg_conv (Conv.abs_conv (fn (_, ctxt) => lambda_prs_conv ctxt quot) ctxt)
-      then_conv (lambda_prs_conv1 ctxt quot)) ctrm
-  | _ $ _ => Conv.comb_conv (lambda_prs_conv ctxt quot) ctrm
-  | Abs _ => Conv.abs_conv (fn (_, ctxt) => lambda_prs_conv ctxt quot) ctxt ctrm
-  | _ => Conv.all_conv ctrm
+fun lambda_prs_conv quot =
+  More_Conv.top_conv (lambda_prs_simple_conv quot) 
 *}
 
 ML {*
-fun lambda_prs_tac ctxt quot = CSUBGOAL (fn (goal, i) =>
-  CONVERSION
+fun lambda_prs_tac quot ctxt = CONVERSION
     (Conv.params_conv ~1 (fn ctxt =>
-       (Conv.prems_conv ~1 (lambda_prs_conv ctxt quot) then_conv
-          Conv.concl_conv ~1 (lambda_prs_conv ctxt quot))) ctxt) i)
+       (Conv.prems_conv ~1 (lambda_prs_conv quot ctxt) then_conv
+          Conv.concl_conv ~1 (lambda_prs_conv quot ctxt))) ctxt) 
 *}
 
 (*
@@ -1170,10 +1166,22 @@
     val simp_ctxt = (Simplifier.context lthy empty_ss) addsimps
       (@{thm eq_reflection[OF fun_map.simps]} :: @{thms id_simps} @ meta_absrep @ meta_reps_same @ defs)
   in
-    EVERY' [TRY o lambda_prs_tac lthy quot,
-            TRY o REPEAT_ALL_NEW (allex_prs_tac lthy quot),
-            TRY o simp_tac simp_ctxt,
-            TRY o rtac refl]
+    EVERY' [
+      
+      (* (Rep1 ---> Abs2) (\<lambda>x. Rep2 (f (Abs1 x)))  ---->  f *)
+      DT lthy "a" (TRY o lambda_prs_tac quot lthy),
+
+      (* \<forall>x\<in>Respects R. (abs ---> id) f  ---->  \<forall>x. f *)
+      DT lthy "b" (TRY o REPEAT_ALL_NEW (allex_prs_tac lthy quot)),
+    
+      (* NewConst  ---->  (rep ---> abs) oldConst *)
+      (* Abs (Rep x)  ---->  x                    *)
+      (* id_simps; fun_map.simps                  *)
+      DT lthy "c" (TRY o simp_tac simp_ctxt),
+
+      (* final step *)
+      DT lthy "d" (TRY o rtac refl)
+    ]
   end
 *}