src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML
changeset 55486 8609527278f2
parent 55480 59cc4a8bc28a
child 55539 0819931d652d
--- a/src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML	Fri Feb 14 17:18:28 2014 +0100
+++ b/src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML	Fri Feb 14 18:42:43 2014 +0100
@@ -268,8 +268,6 @@
 
 fun retypargs tyargs (Type (s, _)) = Type (s, tyargs);
 
-fun exists_strict_subtype_in Ts T = exists_subtype_in (filter_out (curry (op =) T) Ts) T;
-
 fun fold_subtype_pairs f (T as Type (s, Ts), U as Type (s', Us)) =
     f (T, U) #> (if s = s' then fold (fold_subtype_pairs f) (Ts ~~ Us) else I)
   | fold_subtype_pairs f TU = f TU;