# HG changeset patch
# User kuncar
# Date 1335199323 -7200
# Node ID bb6b147c65315f242c0a2857fc90948a04b12256
# Parent  18202d3d58321936226ac578d75326455340548f
added useful Trueprop_conv

diff -r 18202d3d5832 -r bb6b147c6531 src/HOL/Tools/Lifting/lifting_def.ML
--- 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
diff -r 18202d3d5832 -r bb6b147c6531 src/HOL/Tools/Lifting/lifting_util.ML
--- a/src/HOL/Tools/Lifting/lifting_util.ML	Mon Apr 23 17:18:18 2012 +0200
+++ b/src/HOL/Tools/Lifting/lifting_util.ML	Mon Apr 23 18:42:03 2012 +0200
@@ -7,6 +7,7 @@
 signature LIFTING_UTIL =
 sig
   val MRSL: thm list * thm -> thm
+  val Trueprop_conv: conv -> conv
 end;
 
 
@@ -17,4 +18,9 @@
 
 fun ants MRSL thm = fold (fn rl => fn thm => rl RS thm) ants thm
 
+fun Trueprop_conv cv ct =
+  (case Thm.term_of ct of
+    Const (@{const_name Trueprop}, _) $ _ => Conv.arg_conv cv ct
+  | _ => raise CTERM ("Trueprop_conv", [ct]))
+
 end;