# HG changeset patch
# User blanchet
# Date 1398487386 -7200
# Node ID e4f363e16bdc84f1f84b50867cef730a6765d609
# Parent  0f5cf342961c6117a151ac3870ef68f6ae74008b
use right set of variables for recursive check

diff -r 0f5cf342961c -r e4f363e16bdc src/HOL/Tools/BNF/bnf_lfp_size.ML
--- a/src/HOL/Tools/BNF/bnf_lfp_size.ML	Sat Apr 26 00:20:53 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_lfp_size.ML	Sat Apr 26 06:43:06 2014 +0200
@@ -126,7 +126,7 @@
       | mk_size_of_typ (T as Type (s, Ts)) =
         if is_pair_C s Ts then
           pair (snd_const T)
-        else if exists (exists_subtype_in As) Ts then
+        else if exists (exists_subtype_in (As @ Cs)) Ts then
           (case Symtab.lookup data s of
             SOME (size_name, (_, size_o_maps as _ :: _)) =>
             let