correct plumbing of proof contexts, so that force_rty_type won't generalize more type variables than it should

--- a/src/HOL/Tools/Lifting/lifting_def.ML	Thu Apr 05 23:22:54 2012 +0200
+++ b/src/HOL/Tools/Lifting/lifting_def.ML	Fri Apr 06 09:35:47 2012 +0200
@@ -265,7 +265,7 @@
 
     val rsp_rel = Lifting_Term.equiv_relation lthy (fastype_of rhs, qty)
     val rty_forced = (domain_type o fastype_of) rsp_rel;
-    val forced_rhs = force_rty_type lthy rty_forced rhs;
+    val forced_rhs = force_rty_type ctxt rty_forced rhs;
     val internal_rsp_tm = HOLogic.mk_Trueprop (rsp_rel $ forced_rhs $ forced_rhs)
     val readable_rsp_thm_eq = mk_readable_rsp_thm_eq internal_rsp_tm lthy
     val maybe_proven_rsp_thm = try_to_prove_refl readable_rsp_thm_eq
@@ -284,8 +284,8 @@
 
   in
     case maybe_proven_rsp_thm of
-      SOME _ => Proof.theorem NONE after_qed [] lthy
-      | NONE =>  Proof.theorem NONE after_qed [[(readable_rsp_tm,[])]] lthy
+      SOME _ => Proof.theorem NONE after_qed [] ctxt
+      | NONE =>  Proof.theorem NONE after_qed [[(readable_rsp_tm,[])]] ctxt
   end
 
 fun quot_thm_err ctxt (rty, qty) pretty_msg =