# HG changeset patch
# User blanchet
# Date 1407406661 -7200
# Node ID 5b9043595b7dcc803aaee8704757802614babb7c
# Parent  8e74998e04b803fe6031a1666957de215943033c
tuning

diff -r 8e74998e04b8 -r 5b9043595b7d src/HOL/Tools/BNF/bnf_lfp_compat.ML
--- a/src/HOL/Tools/BNF/bnf_lfp_compat.ML	Thu Aug 07 09:35:31 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_lfp_compat.ML	Thu Aug 07 12:17:41 2014 +0200
@@ -90,7 +90,7 @@
             else
               (case Symtab.lookup all_infos T_name1 of
                 SOME {descr, ...} =>
-                length (filter_out (fn (_, (_, Us, _)) => exists Datatype_Aux.is_rec_type Us) descr)
+                length (filter_out (exists Datatype_Aux.is_rec_type o #2 o snd) descr)
               | NONE => raise Fail "unknown old-style datatype");
         in
           chop nn full_descr ||> cliquify_descr |> op ::