--- a/src/HOL/Tools/Lifting/lifting_util.ML Fri Feb 23 14:12:48 2018 +0100
+++ b/src/HOL/Tools/Lifting/lifting_util.ML Fri Feb 23 14:32:59 2018 +0100
@@ -25,7 +25,6 @@
val get_args: int -> term -> term list
val strip_args: int -> term -> term
val all_args_conv: conv -> conv
- val is_Type: typ -> bool
val same_type_constrs: typ * typ -> bool
val Targs: typ -> typ list
val Tname: typ -> string
@@ -108,9 +107,6 @@
fun all_args_conv conv ctm = Conv.try_conv (Conv.combination_conv (all_args_conv conv) conv) ctm
-fun is_Type (Type _) = true
- | is_Type _ = false
-
fun same_type_constrs (Type (r, _), Type (q, _)) = (r = q)
| same_type_constrs _ = false