src/HOL/Tools/Quickcheck/random_generators.ML
changeset 59621 291934bac95e
parent 59617 b60e65ad13df
child 59637 f643308472ce
     1.1 --- a/src/HOL/Tools/Quickcheck/random_generators.ML	Fri Mar 06 14:01:08 2015 +0100
     1.2 +++ b/src/HOL/Tools/Quickcheck/random_generators.ML	Fri Mar 06 15:58:56 2015 +0100
     1.3 @@ -88,7 +88,7 @@
     1.4      val ((t_random_aux as Free (random_aux, T)) $ (t_k as Free (v, _)), proto_t_rhs) =
     1.5        (HOLogic.dest_eq o HOLogic.dest_Trueprop) eq;
     1.6      val Type (_, [_, iT]) = T;
     1.7 -    val icT = Thm.ctyp_of thy iT;
     1.8 +    val icT = Thm.global_ctyp_of thy iT;
     1.9      val inst = Thm.instantiate_cterm ([(aT, icT)], []);
    1.10      fun subst_v t' = map_aterms (fn t as Free (w, _) => if v = w then t' else t | t => t);
    1.11      val t_rhs = lambda t_k proto_t_rhs;
    1.12 @@ -103,7 +103,7 @@
    1.13      val rule = @{thm random_aux_rec}
    1.14        |> Drule.instantiate_normalize
    1.15          ([(aT, icT)],
    1.16 -          [(cT_random_aux, Thm.cterm_of thy t_random_aux), (cT_rhs, Thm.cterm_of thy t_rhs)]);
    1.17 +          [(cT_random_aux, Thm.global_cterm_of thy t_random_aux), (cT_rhs, Thm.global_cterm_of thy t_rhs)]);
    1.18      fun tac ctxt =
    1.19        ALLGOALS (rtac rule)
    1.20        THEN ALLGOALS (simp_tac (put_simpset rew_ss ctxt))