--- a/QuotMain.thy	Sat Nov 28 07:44:17 2009 +0100
+++ b/QuotMain.thy	Sat Nov 28 08:04:23 2009 +0100
@@ -1066,6 +1066,19 @@
 It proves the QUOTIENT assumptions by calling quotient_tac
  *)
 ML {*
+fun make_inst lhs t =
+  let
+    val _ $ (Abs (_, _, (f as Var (_, Type ("fun", [T, _]))) $ u)) = lhs;
+    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;
+
 fun lambda_prs_conv1 ctxt quot_thms ctrm =
   case (term_of ctrm) of ((Const (@{const_name "fun_map"}, _) $ r1 $ a2) $ (Abs _)) =>
   let
@@ -1083,21 +1096,16 @@
     val t = Goal.prove_internal [] gc (fn _ => tac 1)
     val te = @{thm eq_reflection} OF [t]
     val ts = MetaSimplifier.rewrite_rule @{thms id_simps} 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)));*)
+    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 _ = writeln (Syntax.string_of_term @{context} (term_of (cprop_of ti)));*)
   in
     Conv.rewr_conv ti ctrm
   end
-(* TODO: We can add a proper error message... *)
-  handle Bind => Conv.all_conv ctrm
-
 *}
 
-(* quot stands for the QUOTIENT theorems: *) 
+(* quot stands for the QUOTIENT theorems: *)
 (* could be potentially all of them       *)
 ML {*
 fun lambda_prs_conv ctxt quot ctrm =
@@ -1122,15 +1130,18 @@
 fun clean_tac lthy quot defs aps =
   let
     val lower = flat (map (add_lower_defs lthy) defs)
+    val meta_lower = map (fn x => @{thm eq_reflection} OF [x]) lower
     val absrep = map (fn x => @{thm QUOTIENT_ABS_REP} OF [x]) quot
     val reps_same = map (fn x => @{thm QUOTIENT_REL_REP} OF [x]) quot
+    val meta_reps_same = map (fn x => @{thm eq_reflection} OF [x]) reps_same
+    val simp_ctxt = (Simplifier.context lthy empty_ss) addsimps (meta_reps_same @ meta_lower)
     val aps_thms = map (applic_prs lthy absrep) aps
   in
-    EVERY' [TRY o REPEAT_ALL_NEW (allex_prs_tac lthy quot),
-            lambda_prs_tac lthy quot,
+    EVERY' [lambda_prs_tac lthy quot,
+            TRY o simp_tac simp_ctxt,
+            TRY o REPEAT_ALL_NEW (allex_prs_tac lthy quot),
             TRY o REPEAT_ALL_NEW (EqSubst.eqsubst_tac lthy [0] aps_thms),
-            TRY o REPEAT_ALL_NEW (EqSubst.eqsubst_tac lthy [0] lower),
-            simp_tac (HOL_ss addsimps reps_same)]
+            rtac refl]
   end
 *}