Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Tools/BNF/bnf_lfp_size.ML
changeset 56737 e4f363e16bdc
parent 56684 d8f32f55e463
child 56966 01637dd1260c 
--- 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
isabelle