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/Quickcheck/random_generators.ML
changeset 81507 08574da77b4a
parent 77879 dd222e2af01a 
--- a/src/HOL/Tools/Quickcheck/random_generators.ML	Fri Nov 29 11:26:17 2024 +0100
+++ b/src/HOL/Tools/Quickcheck/random_generators.ML	Fri Nov 29 17:40:15 2024 +0100
@@ -219,7 +219,7 @@
         val tTs = (map o apsnd) termifyT simple_tTs;
         val is_rec = exists is_some ks;
         val k = fold (fn NONE => I | SOME k => Integer.max k) ks 0;
-        val vs = Name.invent_names Name.context "x" (map snd simple_tTs);
+        val vs = Name.invent_names_global "x" (map snd simple_tTs);
         val tc = HOLogic.mk_return T \<^typ>\<open>Random.seed\<close>
           (HOLogic.mk_valtermify_app c vs simpleT);
         val t = HOLogic.mk_ST
isabelle