unused;
authorwenzelm
Tue Jun 04 17:04:25 2019 +0200 (6 weeks ago)
changeset 703232943934a169d
parent 70322 65b880d4efbb
child 70324 005c1cdbfd3f
unused;
src/HOL/Tools/Lifting/lifting_util.ML
     1.1 --- a/src/HOL/Tools/Lifting/lifting_util.ML	Tue Jun 04 17:04:18 2019 +0200
     1.2 +++ b/src/HOL/Tools/Lifting/lifting_util.ML	Tue Jun 04 17:04:25 2019 +0200
     1.3 @@ -7,7 +7,6 @@
     1.4  signature LIFTING_UTIL =
     1.5  sig
     1.6    val MRSL: thm list * thm -> thm
     1.7 -  val option_fold: 'b -> ('a -> 'b) -> 'a option -> 'b
     1.8    val dest_Quotient: term -> term * term * term * term
     1.9  
    1.10    val quot_thm_rel: thm -> term
    1.11 @@ -41,9 +40,6 @@
    1.12  
    1.13  fun ants MRSL thm = fold (fn rl => fn thm => rl RS thm) ants thm
    1.14  
    1.15 -fun option_fold a _ NONE = a
    1.16 -  | option_fold _ f (SOME x) = f x
    1.17 -
    1.18  fun dest_Quotient (Const (\<^const_name>\<open>Quotient\<close>, _) $ rel $ abs $ rep $ cr)
    1.19        = (rel, abs, rep, cr)
    1.20    | dest_Quotient t = raise TERM ("dest_Quotient", [t])