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/inductive_codegen.ML
changeset 33049 c38f02fdf35d
parent 33038 8f9594c31de4
child 33050 fe166e8b9f07 
--- a/src/HOL/Tools/inductive_codegen.ML	Wed Oct 21 10:15:31 2009 +0200
+++ b/src/HOL/Tools/inductive_codegen.ML	Wed Oct 21 12:09:37 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) =>
isabelle