--- a/src/HOL/Tools/Lifting/lifting_util.ML Tue Jun 04 17:04:18 2019 +0200
+++ b/src/HOL/Tools/Lifting/lifting_util.ML Tue Jun 04 17:04:25 2019 +0200
@@ -7,7 +7,6 @@
signature LIFTING_UTIL =
sig
val MRSL: thm list * thm -> thm
- val option_fold: 'b -> ('a -> 'b) -> 'a option -> 'b
val dest_Quotient: term -> term * term * term * term
val quot_thm_rel: thm -> term
@@ -41,9 +40,6 @@
fun ants MRSL thm = fold (fn rl => fn thm => rl RS thm) ants thm
-fun option_fold a _ NONE = a
- | option_fold _ f (SOME x) = f x
-
fun dest_Quotient (Const (\<^const_name>\<open>Quotient\<close>, _) $ rel $ abs $ rep $ cr)
= (rel, abs, rep, cr)
| dest_Quotient t = raise TERM ("dest_Quotient", [t])