# HG changeset patch
# User wenzelm
# Date 1377524751 -7200
# Node ID 8d41170242cb23b578d77a8719016226dd7393ee
# Parent  2333fae25719de67d9c1956d6b18538b53cc926d
proper context;

diff -r 2333fae25719 -r 8d41170242cb src/HOL/Tools/Lifting/lifting_def.ML
--- a/src/HOL/Tools/Lifting/lifting_def.ML	Mon Aug 26 12:14:41 2013 +0200
+++ b/src/HOL/Tools/Lifting/lifting_def.ML	Mon Aug 26 15:45:51 2013 +0200
@@ -414,7 +414,7 @@
     val ((_, (_ , def_thm)), lthy') = 
       Local_Theory.define (var, ((Thm.def_binding (#1 var), []), newrhs)) lthy
 
-    val transfer_rule = generate_transfer_rule lthy quot_thm rsp_thm def_thm opt_par_thm
+    val transfer_rule = generate_transfer_rule lthy' quot_thm rsp_thm def_thm opt_par_thm
 
     val abs_eq_thm = generate_abs_eq lthy' def_thm rsp_thm quot_thm
     val opt_rep_eq_thm = generate_rep_eq lthy' def_thm rsp_thm (rty_forced, qty)