# 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)