use right set of variables for recursive check

--- 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