# HG changeset patch
# User kuncar
# Date 1393505553 -3600
# Node ID cbeb32e44ff1d4d5d134b8ebfcf4083baa7b2b29
# Parent  367ec44763fdfce599f39c6015cb6452e5e0a0a2
hide Lifting.invariant from a user completely

diff -r 367ec44763fd -r cbeb32e44ff1 src/HOL/Tools/Lifting/lifting_def.ML
--- a/src/HOL/Tools/Lifting/lifting_def.ML	Thu Feb 27 13:04:57 2014 +0100
+++ b/src/HOL/Tools/Lifting/lifting_def.ML	Thu Feb 27 13:52:33 2014 +0100
@@ -530,12 +530,16 @@
     val unfold_ret_val_invs = Conv.bottom_conv 
       (K (Conv.try_conv (Conv.rewr_conv @{thm invariant_same_args}))) lthy
     val cr_to_pcr_conv = Raw_Simplifier.rewrite lthy false (get_cr_pcr_eqs lthy)
-    val simp_conv = HOLogic.Trueprop_conv (Conv.fun2_conv (cr_to_pcr_conv then_conv simp_arrows_conv))
+    val unfold_inv_conv = 
+      Conv.top_sweep_conv (K (Conv.rewr_conv @{thm invariant_def[THEN eq_reflection]})) lthy
+    val simp_conv = HOLogic.Trueprop_conv (Conv.fun2_conv 
+      (cr_to_pcr_conv then_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
     val eq_thm = 
-      (simp_conv then_conv univq_prenex_conv then_conv beta_conv then_conv unfold_ret_val_invs) ctm
+      (simp_conv then_conv univq_prenex_conv then_conv beta_conv then_conv unfold_ret_val_invs
+         then_conv unfold_inv_conv) ctm
   in
     Object_Logic.rulify lthy (eq_thm RS Drule.equal_elim_rule2)
   end