--- a/src/HOL/Tools/Quickcheck/random_generators.ML Fri Apr 10 14:44:08 2015 +0200
+++ b/src/HOL/Tools/Quickcheck/random_generators.ML Fri Apr 10 18:23:01 2015 +0200
@@ -96,7 +96,7 @@
subst_v (@{const Code_Numeral.Suc} $ t_k) eq];
val eqs1 = map (Pattern.rewrite_term thy rew_ts []) eqs0;
val ((_, (_, eqs2)), lthy') = lthy
- |> BNF_LFP_Compat.add_primrec_simple
+ |> BNF_LFP_Compat.primrec_simple
[((Binding.concealed (Binding.name random_aux), T), NoSyn)] eqs1;
val cT_random_aux = inst pt_random_aux;
val cT_rhs = inst pt_rhs;