| changeset 33050 | fe166e8b9f07 |
| parent 33042 | ddf1f03a9ad9 |
| parent 33049 | c38f02fdf35d |
| child 33063 | 4d462963a7db |
--- a/src/HOL/Tools/inductive_codegen.ML Wed Oct 21 12:08:52 2009 +0200 +++ b/src/HOL/Tools/inductive_codegen.ML Wed Oct 21 12:12:21 2009 +0200 @@ -482,7 +482,7 @@ fun constrain cs [] = [] | constrain cs ((s, xs) :: ys) = (s, case AList.lookup (op =) cs (s : string) of NONE => xs - | SOME xs' => inter (op =) (xs, xs')) :: constrain cs ys; + | SOME xs' => inter (op =) xs' xs) :: constrain cs ys; fun mk_extra_defs thy defs gr dep names module ts = Library.foldl (fn (gr, name) =>