src/HOL/BNF/Tools/bnf_lfp_compat.ML
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;