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;