src/HOL/Tools/Quickcheck/random_generators.ML

         val t = HOLogic.mk_ST
           (map2 (fn (t, _) => fn (v, T') => ((t, @{typ Random.seed}), SOME ((v, termifyT T')))) tTs vs)
             tc @{typ Random.seed} (SOME T, @{typ Random.seed});
         val tk = if is_rec
           then if k = 0 then size
-            else @{term "Quickcheck.beyond :: code_numeral \<Rightarrow> code_numeral \<Rightarrow> code_numeral"}
+            else @{term "Quickcheck_Random.beyond :: code_numeral \<Rightarrow> code_numeral \<Rightarrow> code_numeral"}
              $ HOLogic.mk_number @{typ code_numeral} k $ size
           else @{term "1::code_numeral"}
       in (is_rec, HOLogic.mk_prod (tk, t)) end;
     fun sort_rec xs =
       map_filter (fn (true, t) => SOME t | _ =>  NONE) xs
       @ map_filter (fn (false, t) => SOME t | _ =>  NONE) xs;
     val gen_exprss = tss
       |> (map o apfst) Type
       |> map (fn (T, cs) => (T, (sort_rec o map (mk_consexpr T)) cs));
     fun mk_select (rT, xs) =
-      mk_const @{const_name Quickcheck.collapse} [@{typ "Random.seed"}, termifyT rT]
+      mk_const @{const_name Quickcheck_Random.collapse} [@{typ Random.seed}, termifyT rT]
       $ (mk_const @{const_name Random.select_weight} [random_resultT rT]
         $ HOLogic.mk_list (HOLogic.mk_prodT (@{typ code_numeral}, random_resultT rT)) xs)
           $ seed;
     val auxs_lhss = map (fn t => t $ size $ size' $ seed) random_auxs;
     val auxs_rhss = map mk_select gen_exprss;

       (@{const_name prod_case}, [T, @{typ "unit => term"}, liftT resultT @{typ Random.seed}]);
     fun mk_scomp_split T t t' =
       mk_scomp (mk_termtyp T) resultT @{typ Random.seed} t
         (mk_split T $ Abs ("", T, Abs ("", @{typ "unit => term"}, t')));
     fun mk_bindclause (_, _, i, T) = mk_scomp_split T
-      (Sign.mk_const thy (@{const_name Quickcheck.random}, [T]) $ Bound i);
+      (Sign.mk_const thy (@{const_name Quickcheck_Random.random}, [T]) $ Bound i);
   in
     lambda genuine_only
       (Abs ("n", @{typ code_numeral}, fold_rev mk_bindclause bounds (return $ check true)))
   end;
 

     val bounds = map_index (fn (i, ty) =>
       (2 * (bound_max - i) + 1, 2 * (bound_max - i), 2 * i, ty)) Ts;
     val prop' = betapplys (prop, map (fn (i, _, _, _) => Bound i) bounds);
     val terms = HOLogic.mk_list @{typ term} (map (fn (_, i, _, _) => Bound i $ @{term "()"}) bounds)
     val (assms, concl) = Quickcheck_Common.strip_imp prop'
-    val return = HOLogic.pair_const resultT @{typ "Random.seed"};
+    val return = HOLogic.pair_const resultT @{typ Random.seed};
     fun mk_assms_report i =
       HOLogic.mk_prod (@{term "None :: (bool * term list) option"},
         HOLogic.mk_prod (HOLogic.mk_list HOLogic.boolT
           (replicate i @{term True} @ replicate (length assms - i) @{term False}),
         @{term False}))

       (@{const_name prod_case}, [T, @{typ "unit => term"}, liftT resultT @{typ Random.seed}]);
     fun mk_scomp_split T t t' =
       mk_scomp (mk_termtyp T) resultT @{typ Random.seed} t
         (mk_split T $ Abs ("", T, Abs ("", @{typ "unit => term"}, t')));
     fun mk_bindclause (_, _, i, T) = mk_scomp_split T
-      (Sign.mk_const thy (@{const_name Quickcheck.random}, [T]) $ Bound i);
+      (Sign.mk_const thy (@{const_name Quickcheck_Random.random}, [T]) $ Bound i);
   in
     lambda genuine_only
       (Abs ("n", @{typ code_numeral}, fold_rev mk_bindclause bounds (return $ check true)))
   end