use right set of variables for recursive check
authorblanchet
Sat Apr 26 06:43:06 2014 +0200 (2014-04-26)
changeset 56737e4f363e16bdc
parent 56736 0f5cf342961c
child 56738 13b0fc4ece42
child 56743 81370dfadb1d
use right set of variables for recursive check
src/HOL/Tools/BNF/bnf_lfp_size.ML
     1.1 --- a/src/HOL/Tools/BNF/bnf_lfp_size.ML	Sat Apr 26 00:20:53 2014 +0200
     1.2 +++ b/src/HOL/Tools/BNF/bnf_lfp_size.ML	Sat Apr 26 06:43:06 2014 +0200
     1.3 @@ -126,7 +126,7 @@
     1.4        | mk_size_of_typ (T as Type (s, Ts)) =
     1.5          if is_pair_C s Ts then
     1.6            pair (snd_const T)
     1.7 -        else if exists (exists_subtype_in As) Ts then
     1.8 +        else if exists (exists_subtype_in (As @ Cs)) Ts then
     1.9            (case Symtab.lookup data s of
    1.10              SOME (size_name, (_, size_o_maps as _ :: _)) =>
    1.11              let