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_rep_proofs.ML
changeset 20071 8f3e1ddb50e6
parent 20046 9c8909fc5865
child 20820 58693343905f 
--- a/src/HOL/Tools/datatype_rep_proofs.ML	Tue Jul 11 12:16:52 2006 +0200
+++ b/src/HOL/Tools/datatype_rep_proofs.ML	Tue Jul 11 12:16:54 2006 +0200
@@ -392,7 +392,7 @@
         fun mk_thm i =
           let
             val Ts = map (TFree o rpair HOLogic.typeS)
-              (variantlist (replicate i "'t", used));
+              (Name.variant_list used (replicate i "'t"));
             val f = Free ("f", Ts ---> U)
           in Goal.prove_global sign [] [] (Logic.mk_implies
             (HOLogic.mk_Trueprop (HOLogic.list_all
isabelle