--- a/Quot/Examples/IntEx.thy	Mon Dec 07 14:35:45 2009 +0100
+++ b/Quot/Examples/IntEx.thy	Mon Dec 07 15:18:00 2009 +0100
@@ -256,13 +256,11 @@
 by simp
 
 
-
-
 lemma "(\<lambda>(y :: my_int). y) = (\<lambda>(x :: my_int). x)"
 apply(tactic {* procedure_tac @{context} @{thm lam_tst2} 1 *})
 defer
 apply(tactic {* all_inj_repabs_tac_intex @{context} 1*})
-(*apply(tactic {* lambda_prs_tac  @{context} 1 *})*)
+apply(tactic {* clean_tac  @{context} 1 *})
 sorry
 
 lemma lam_tst3: "(\<lambda>(y :: nat \<times> nat \<Rightarrow> nat \<times> nat). y) = (\<lambda>(x :: nat \<times> nat \<Rightarrow> nat \<times> nat). x)"
@@ -272,5 +270,5 @@
 apply(tactic {* procedure_tac @{context} @{thm lam_tst3} 1 *})
 defer
 apply(tactic {* all_inj_repabs_tac_intex @{context} 1*})
-apply(tactic {* lambda_prs_tac  @{context} 1 *})
+apply(tactic {* clean_tac  @{context} 1 *})
 sorry

--- a/Quot/QuotMain.thy	Mon Dec 07 14:35:45 2009 +0100
+++ b/Quot/QuotMain.thy	Mon Dec 07 15:18:00 2009 +0100
@@ -980,10 +980,27 @@
   in (f, Abs ("x", T, mk_abs 0 g)) end;
 *}
 
+(* Since the patterns for the lhs are different; there are 2 different make-insts *)
+ML {*
+fun make_inst2 lhs t =
+  let
+    val _ $ (Abs (_, _, (_ $ ((f as Var (_, Type ("fun", [T, _]))) $ u)))) = lhs;
+    val _ = tracing "a";
+    val _ $ (Abs (_, _, (_ $ g))) = t;
+    fun mk_abs i t =
+      if incr_boundvars i u aconv t then Bound i
+      else (case t of
+        t1 $ t2 => mk_abs i t1 $ mk_abs i t2
+      | Abs (s, T, t') => Abs (s, T, mk_abs (i + 1) t')
+      | Bound j => if i = j then error "make_inst" else t
+      | _ => t);
+  in (f, Abs ("x", T, mk_abs 0 g)) end;
+*}
+
 ML {*
 fun lambda_prs_simple_conv ctxt ctrm =
   case (term_of ctrm) of
-   ((Const (@{const_name fun_map}, _) $ r1 $ (a2 as (Const (s,_)))) $ (Abs _)) =>
+   ((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)
@@ -992,18 +1009,26 @@
        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 _ = tracing ("te rule:\n" ^ (Syntax.string_of_term ctxt (prop_of 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 _ = if not (s = @{const_name "id"}) then
+       val ti =
+         (let
+           val ts = MetaSimplifier.rewrite_rule @{thms id_simps} te
+           val (insp, inst) = make_inst (term_of (Thm.lhs_of ts)) (term_of ctrm)
+         in
+           Drule.instantiate ([], [(cterm_of thy insp, cterm_of thy inst)]) ts
+         end handle Bind =>
+         let
+           val (insp, inst) = make_inst2 (term_of (Thm.lhs_of te)) (term_of ctrm)
+           val td = Drule.instantiate ([], [(cterm_of thy insp, cterm_of thy inst)]) te
+         in
+           MetaSimplifier.rewrite_rule @{thms id_simps} td
+         end);
+       val _ = if not (Term.is_Const a2 andalso fst (dest_Const a2) = @{const_name "id"}) then
                   (tracing "lambda_prs";
                    tracing ("redex:\n" ^ (Syntax.string_of_term ctxt (term_of ctrm)));
                    tracing ("lpi rule:\n" ^ (Syntax.string_of_term ctxt (prop_of lpi)));
                    tracing ("te rule:\n" ^ (Syntax.string_of_term ctxt (prop_of te)));
-                   tracing ("ts rule:\n" ^ (Syntax.string_of_term ctxt (prop_of ts)));
-                   tracing ("instantiated rule:\n" ^ (Syntax.string_of_term ctxt (prop_of ti))))
+                   tracing ("ti rule:\n" ^ (Syntax.string_of_term ctxt (prop_of ti))))
                else ()
      in
        Conv.rewr_conv ti ctrm