diff -r f7dee6e808eb -r e99c0334d8bf QuotMain.thy
--- a/QuotMain.thy	Wed Nov 25 03:47:07 2009 +0100
+++ b/QuotMain.thy	Wed Nov 25 10:34:03 2009 +0100
@@ -1649,9 +1649,51 @@
 *}
 
 ML {*
-fun lambda_prs_tac lthy quot =
-  (EqSubst.eqsubst_tac lthy [0] @{thms LAMBDA_PRS}
-  THEN' (RANGE [quotient_tac quot, quotient_tac quot]));
+fun lambda_prs_conv1 ctxt quot 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);
+    val (_, [ty_c, ty_d]) = dest_Type (fastype_of a2);
+    val thy = ProofContext.theory_of ctxt;
+    val [cty_a, cty_b, cty_c, cty_d] = map (ctyp_of thy) [ty_a, ty_b, ty_c, ty_d]
+    val tyinst = [SOME cty_a, SOME cty_b, SOME cty_c, SOME cty_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 tac =
+      (compose_tac (false, lpi, 2)) THEN_ALL_NEW
+      (quotient_tac quot);
+    val gc = Drule.strip_imp_concl (cprop_of lpi);
+    val t = Goal.prove_internal [] gc (fn _ => tac 1)
+    val te = @{thm eq_reflection} OF [t]
+    val ts = MetaSimplifier.rewrite_rule [@{thm eq_reflection} OF @{thms id_apply}] te
+    val tl = Thm.lhs_of ts
+(*    val _ = tracing (Syntax.string_of_term @{context} (term_of ctrm));*)
+(*    val _ = tracing (Syntax.string_of_term @{context} (term_of tl));*)
+    val insts = matching_prs (ProofContext.theory_of ctxt) (term_of tl) (term_of ctrm);
+    val ti = Drule.eta_contraction_rule (Drule.instantiate insts ts);
+(*    val _ = tracing (Syntax.string_of_term @{context} (term_of (cprop_of ti)));*)
+  in
+    Conv.rewr_conv ti ctrm
+  end
+
+*}
+ML {*
+fun lambda_prs_conv ctxt quot ctrm =
+  case (term_of ctrm) of
+    (Const (@{const_name "fun_map"}, _) $ r1 $ a2) $ (Abs (_, _, x)) =>
+      (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
+*}
+
+ML {*
+fun lambda_prs_tac ctxt quot = CSUBGOAL (fn (goal, i) =>
+  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)
 *}
 
 ML {*
@@ -1664,7 +1706,7 @@
     val lower = flat (map (add_lower_defs lthy) defs)
   in
     TRY' (REPEAT_ALL_NEW (allex_prs_tac lthy quot)) THEN'
-    TRY' (REPEAT_ALL_NEW (lambda_prs_tac lthy quot)) THEN'
+    TRY' (lambda_prs_tac lthy quot) THEN'
     TRY' (REPEAT_ALL_NEW (EqSubst.eqsubst_tac lthy [0] lower)) THEN'
     simp_tac (HOL_ss addsimps [reps_same])
   end