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/datatype_codegen.ML
changeset 20071 8f3e1ddb50e6
parent 19886 6bec6daac280
child 20105 454f4be984b7 
--- a/src/HOL/Tools/datatype_codegen.ML	Tue Jul 11 12:16:52 2006 +0200
+++ b/src/HOL/Tools/datatype_codegen.ML	Tue Jul 11 12:16:54 2006 +0200
@@ -219,7 +219,7 @@
           | pcase gr ((cname, cargs)::cs) (t::ts) (U::Us) =
               let
                 val j = length cargs;
-                val xs = variantlist (replicate j "x", names);
+                val xs = Name.variant_list names (replicate j "x");
                 val Us' = Library.take (j, fst (strip_type U));
                 val frees = map Free (xs ~~ Us');
                 val (gr0, cp) = invoke_codegen thy defs dep module false
isabelle