--- a/src/HOL/Tools/Lifting/lifting_def.ML Mon Apr 23 17:18:18 2012 +0200
+++ b/src/HOL/Tools/Lifting/lifting_def.ML Mon Apr 23 18:42:03 2012 +0200
@@ -240,7 +240,7 @@
val unfold_ret_val_invs = Conv.bottom_conv
(K (Conv.try_conv (Conv.rewr_conv @{thm invariant_same_args}))) lthy
- val simp_conv = Conv.arg_conv (Conv.fun2_conv simp_arrows_conv)
+ val simp_conv = Trueprop_conv (Conv.fun2_conv simp_arrows_conv)
val univq_conv = Conv.rewr_conv @{thm HOL.all_simps(6)[symmetric, THEN eq_reflection]}
val univq_prenex_conv = Conv.top_conv (K (Conv.try_conv univq_conv)) lthy
val beta_conv = Thm.beta_conversion true