# HG changeset patch
# User huffman
# Date 1333697747 -7200
# Node ID c608111857d19e22c45b4a1670b02c5154afc11e
# Parent  075d22b3a32f0e9825d6ab46b56275ecd4d829db
correct plumbing of proof contexts, so that force_rty_type won't generalize more type variables than it should

diff -r 075d22b3a32f -r c608111857d1 src/HOL/Tools/Lifting/lifting_def.ML
--- 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 =