# HG changeset patch # User wenzelm # Date 1519412019 -3600 # Node ID 350f0579d343b2d90c83f6474f856d2d45e1f965 # Parent 951f96d386cf067569523db8e3b7f54ab5006dda removed unused clone of (map o apsnd); removed unused variant of HOLogic.mk_obj_eq; diff -r 951f96d386cf -r 350f0579d343 src/HOL/Tools/Lifting/lifting_util.ML --- a/src/HOL/Tools/Lifting/lifting_util.ML Fri Feb 23 19:36:16 2018 +0100 +++ b/src/HOL/Tools/Lifting/lifting_util.ML Fri Feb 23 19:53:39 2018 +0100 @@ -8,7 +8,6 @@ sig val MRSL: thm list * thm -> thm val option_fold: 'b -> ('a -> 'b) -> 'a option -> 'b - val map_snd: ('b -> 'c) -> ('a * 'b) list -> ('a * 'c) list val dest_Quotient: term -> term * term * term * term val quot_thm_rel: thm -> term @@ -30,7 +29,6 @@ val Tname: typ -> string val is_rel_fun: term -> bool val relation_types: typ -> typ * typ - val safe_HOL_meta_eq: thm -> thm val map_interrupt: ('a -> 'b option) -> 'a list -> 'b list option val conceal_naming_result: (local_theory -> 'a * local_theory) -> local_theory -> 'a * local_theory end @@ -46,8 +44,6 @@ fun option_fold a _ NONE = a | option_fold _ f (SOME x) = f x -fun map_snd f xs = map (fn (a, b) => (a, f b)) xs - fun dest_Quotient (Const (@{const_name Quotient}, _) $ rel $ abs $ rep $ cr) = (rel, abs, rep, cr) | dest_Quotient t = raise TERM ("dest_Quotient", [t]) @@ -121,8 +117,6 @@ ([typ1, typ2], @{typ bool}) => (typ1, typ2) | _ => error "relation_types: not a relation" -fun safe_HOL_meta_eq r = HOLogic.mk_obj_eq r handle Thm.THM _ => r - fun map_interrupt f l = let fun map_interrupt' _ [] l = SOME (rev l)