--- a/src/HOL/Tools/Lifting/lifting_util.ML Thu Feb 28 16:38:17 2013 +0100
+++ b/src/HOL/Tools/Lifting/lifting_util.ML Thu Feb 28 16:54:52 2013 +0100
@@ -7,7 +7,6 @@
signature LIFTING_UTIL =
sig
val MRSL: thm list * thm -> thm
- val Trueprop_conv: conv -> conv
val option_fold: 'b -> ('a -> 'b) -> 'a option -> 'b
val dest_Quotient: term -> term * term * term * term
@@ -26,11 +25,6 @@
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]))
-
fun option_fold a _ NONE = a
| option_fold _ f (SOME x) = f x