--- 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)