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/split_rule.ML
changeset 20071 8f3e1ddb50e6
parent 19735 ff13585fbdab
child 22278 70a7cd02fec1 
--- a/src/HOL/Tools/split_rule.ML	Tue Jul 11 12:16:52 2006 +0200
+++ b/src/HOL/Tools/split_rule.ML	Tue Jul 11 12:16:54 2006 +0200
@@ -81,7 +81,7 @@
         fun mk_tuple (v as Var ((a, _), T)) (xs, insts) =
               let
                 val Ts = HOLogic.prodT_factors T;
-                val ys = Term.variantlist (replicate (length Ts) a, xs);
+                val ys = Name.variant_list xs (replicate (length Ts) a);
               in (xs @ ys, (cterm v, cterm (HOLogic.mk_tuple T
                 (map (Var o apfst (rpair 0)) (ys ~~ Ts))))::insts)
               end
isabelle