# HG changeset patch
# User wenzelm
# Date 1723290136 -7200
# Node ID d517afba4968b28f5c44654385e3e198aebfe779
# Parent  fd69f98e218284dc0b3327f5db96259464ef070c
unused;

diff -r fd69f98e2182 -r d517afba4968 src/HOL/Tools/Lifting/lifting_util.ML
--- a/src/HOL/Tools/Lifting/lifting_util.ML	Sat Aug 10 12:26:17 2024 +0200
+++ b/src/HOL/Tools/Lifting/lifting_util.ML	Sat Aug 10 13:42:16 2024 +0200
@@ -20,13 +20,11 @@
 
   val undisch: thm -> thm
   val undisch_all: thm -> thm
-  val is_fun_type: typ -> bool
   val get_args: int -> term -> term list
   val strip_args: int -> term -> term
   val all_args_conv: conv -> conv
   val Targs: typ -> typ list
   val Tname: typ -> string
-  val is_rel_fun: term -> bool
   val relation_types: typ -> typ * typ
   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
@@ -90,9 +88,6 @@
 
 fun undisch_all thm = funpow (Thm.nprems_of thm) undisch thm
 
-fun is_fun_type (Type (\<^type_name>\<open>fun\<close>, _)) = true
-  | is_fun_type _ = false
-
 fun get_args n = rev o fst o funpow_yield n (swap o dest_comb)
 
 fun strip_args n = funpow n (fst o dest_comb)
@@ -105,9 +100,6 @@
 fun Tname (Type (name, _)) = name
   | Tname _ = ""
 
-fun is_rel_fun (Const (\<^const_name>\<open>rel_fun\<close>, _) $ _ $ _) = true
-  | is_rel_fun _ = false
-
 fun relation_types typ = 
   case strip_type typ of
     ([typ1, typ2], \<^typ>\<open>bool\<close>) => (typ1, typ2)