# HG changeset patch
# User wenzelm
# Date 1425682432 -3600
# Node ID f643308472ce98e64654049b45e7e20216cae0b9
# Parent  9f44d053b97256618a391e216303d012d6ef762c
clarified context;

diff -r 9f44d053b972 -r f643308472ce src/HOL/Tools/Quickcheck/random_generators.ML
--- a/src/HOL/Tools/Quickcheck/random_generators.ML	Fri Mar 06 23:53:36 2015 +0100
+++ b/src/HOL/Tools/Quickcheck/random_generators.ML	Fri Mar 06 23:53:52 2015 +0100
@@ -88,7 +88,7 @@
     val ((t_random_aux as Free (random_aux, T)) $ (t_k as Free (v, _)), proto_t_rhs) =
       (HOLogic.dest_eq o HOLogic.dest_Trueprop) eq;
     val Type (_, [_, iT]) = T;
-    val icT = Thm.global_ctyp_of thy iT;
+    val icT = Thm.ctyp_of lthy iT;
     val inst = Thm.instantiate_cterm ([(aT, icT)], []);
     fun subst_v t' = map_aterms (fn t as Free (w, _) => if v = w then t' else t | t => t);
     val t_rhs = lambda t_k proto_t_rhs;
@@ -103,7 +103,8 @@
     val rule = @{thm random_aux_rec}
       |> Drule.instantiate_normalize
         ([(aT, icT)],
-          [(cT_random_aux, Thm.global_cterm_of thy t_random_aux), (cT_rhs, Thm.global_cterm_of thy t_rhs)]);
+          [(cT_random_aux, Thm.cterm_of lthy' t_random_aux),
+           (cT_rhs, Thm.cterm_of lthy' t_rhs)]);
     fun tac ctxt =
       ALLGOALS (rtac rule)
       THEN ALLGOALS (simp_tac (put_simpset rew_ss ctxt))