1.1 --- a/src/HOL/Tools/quickcheck_generators.ML	Wed Feb 17 11:21:59 2010 +0100
     1.2 +++ b/src/HOL/Tools/quickcheck_generators.ML	Wed Feb 17 13:48:13 2010 +0100
     1.3 @@ -139,7 +139,7 @@
     1.4      val eqs0 = [subst_v @{term "0::code_numeral"} eq,
     1.5        subst_v (@{term "Suc_code_numeral"} $ t_k) eq];
     1.6      val eqs1 = map (Pattern.rewrite_term thy rew_ts []) eqs0;
     1.7 -    val ((_, eqs2), lthy') = Primrec.add_primrec_simple
     1.8 +    val ((_, (_, eqs2)), lthy') = Primrec.add_primrec_simple
     1.9        [((Binding.conceal (Binding.name random_aux), T), NoSyn)] eqs1 lthy;
    1.10      val cT_random_aux = inst pt_random_aux;
    1.11      val cT_rhs = inst pt_rhs;
    1.12 @@ -148,7 +148,7 @@
    1.13             [(cT_random_aux, cert t_random_aux), (cT_rhs, cert t_rhs)]);
    1.14      val tac = ALLGOALS (rtac rule)
    1.15        THEN ALLGOALS (simp_tac rew_ss)
    1.16 -      THEN (ALLGOALS (ProofContext.fact_tac (flat eqs2)))
    1.17 +      THEN (ALLGOALS (ProofContext.fact_tac eqs2))
    1.18      val simp = Skip_Proof.prove lthy' [v] [] eq (K tac);
    1.19    in (simp, lthy') end;
    1.20