diff -r eb59c6968219 -r b60e65ad13df src/HOL/Tools/Quickcheck/random_generators.ML
--- a/src/HOL/Tools/Quickcheck/random_generators.ML	Thu Mar 05 13:28:04 2015 +0100
+++ b/src/HOL/Tools/Quickcheck/random_generators.ML	Fri Mar 06 00:00:57 2015 +0100
@@ -89,24 +89,25 @@
       (HOLogic.dest_eq o HOLogic.dest_Trueprop) eq;
     val Type (_, [_, iT]) = T;
     val icT = Thm.ctyp_of thy iT;
-    val cert = Thm.cterm_of thy;
     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;
     val eqs0 = [subst_v @{term "0::natural"} eq,
       subst_v (@{const Code_Numeral.Suc} $ t_k) eq];
     val eqs1 = map (Pattern.rewrite_term thy rew_ts []) eqs0;
-    val ((_, (_, eqs2)), lthy') = BNF_LFP_Compat.add_primrec_simple
-      [((Binding.conceal (Binding.name random_aux), T), NoSyn)] eqs1 lthy;
+    val ((_, (_, eqs2)), lthy') = lthy
+      |> BNF_LFP_Compat.add_primrec_simple
+        [((Binding.conceal (Binding.name random_aux), T), NoSyn)] eqs1;
     val cT_random_aux = inst pt_random_aux;
     val cT_rhs = inst pt_rhs;
     val rule = @{thm random_aux_rec}
-      |> Drule.instantiate_normalize ([(aT, icT)],
-           [(cT_random_aux, cert t_random_aux), (cT_rhs, cert t_rhs)]);
+      |> Drule.instantiate_normalize
+        ([(aT, icT)],
+          [(cT_random_aux, Thm.cterm_of thy t_random_aux), (cT_rhs, Thm.cterm_of thy t_rhs)]);
     fun tac ctxt =
       ALLGOALS (rtac rule)
       THEN ALLGOALS (simp_tac (put_simpset rew_ss ctxt))
-      THEN (ALLGOALS (Proof_Context.fact_tac ctxt eqs2))
+      THEN (ALLGOALS (Proof_Context.fact_tac ctxt eqs2));
     val simp = Goal.prove_sorry lthy' [v] [] eq (tac o #context);
   in (simp, lthy') end;