diff -r ca1a24aa822e -r b97f3f5fbc18 QuotMain.thy
--- a/QuotMain.thy	Mon Oct 26 11:55:36 2009 +0100
+++ b/QuotMain.thy	Mon Oct 26 13:33:28 2009 +0100
@@ -709,6 +709,7 @@
     ),
     (instantiate_tac @{thm REP_ABS_RSP(1)} ctxt THEN' (RANGE [quotient_tac quot_thm])),
     rtac refl,
+    rtac @{thm arg_cong2[of _ _ _ _ "op ="]},
     (instantiate_tac @{thm APPLY_RSP} ctxt THEN' (RANGE [quotient_tac quot_thm, quotient_tac quot_thm])),
     rtac reflex_thm,
     atac,
@@ -787,5 +788,19 @@
   end
 *}
 
+text {* the proper way to do it *}
+ML {*
+  fun findabs rty tm =
+    case tm of
+      Abs(_, T, b) =>
+        let
+          val b' = subst_bound ((Free ("x", T)), b);
+          val tys = findabs rty b'
+          val ty = fastype_of tm
+        in if needs_lift rty ty then (ty :: tys) else tys
+        end
+    | f $ a => (findabs rty f) @ (findabs rty a)
+    | _ => []
+*}
 
 end