# HG changeset patch
# User wenzelm
# Date 1559660665 -7200
# Node ID 2943934a169d4c3a3df23d0aca356b9f14b346b4
# Parent  65b880d4efbbcc259425793196675a017963dbe8
unused;

diff -r 65b880d4efbb -r 2943934a169d src/HOL/Tools/Lifting/lifting_util.ML
--- 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])