--- a/src/HOL/Tools/Quickcheck/exhaustive_generators.ML Mon Mar 14 12:34:11 2011 +0100
+++ b/src/HOL/Tools/Quickcheck/exhaustive_generators.ML Mon Mar 14 12:34:12 2011 +0100
@@ -193,7 +193,7 @@
#> apfst fst) (exhaustivesN ~~ (Ts @ Us))
#> (fn (exhaustives, lthy) =>
let
- val eqs_t = mk_equations thy descr vs tycos exhaustives (Ts, Us)
+ val eqs_t = mk_equations descr vs tycos exhaustives (Ts, Us)
val eqs = map (fn eq => Goal.prove lthy ["f", "i"] [] eq
(fn _ => Skip_Proof.cheat_tac (ProofContext.theory_of lthy))) eqs_t
in