changeset 53901 | 3d93e8b4ae02 |
parent 53808 | b3e2022530e3 |
child 54003 | c4343c31f86d |
--- a/src/HOL/BNF/Tools/bnf_lfp_compat.ML Thu Sep 26 01:05:06 2013 +0200 +++ b/src/HOL/BNF/Tools/bnf_lfp_compat.ML Thu Sep 26 01:05:07 2013 +0200 @@ -67,7 +67,7 @@ val mutual_Ts = map substT mutual_Ts0; - fun add_interesting_subtypes (U as Type (s, Us)) = + fun add_interesting_subtypes (U as Type (_, Us)) = (case filter (exists_subtype_in mutual_Ts) Us of [] => I | Us' => insert (op =) U #> fold add_interesting_subtypes Us') | add_interesting_subtypes _ = I;