--- a/src/HOL/Tools/quickcheck_generators.ML Mon Jun 15 11:01:18 2009 +0200
+++ b/src/HOL/Tools/quickcheck_generators.ML Mon Jun 15 17:36:49 2009 +0200
@@ -212,7 +212,7 @@
fun prove_eqs aux_simp proj_defs lthy =
let
val proj_simps = map (snd o snd) proj_defs;
- fun tac { context = ctxt, ... } =
+ fun tac { context = ctxt, prems = _ } =
ALLGOALS (simp_tac (HOL_ss addsimps proj_simps))
THEN ALLGOALS (EqSubst.eqsubst_tac ctxt [0] [aux_simp])
THEN ALLGOALS (simp_tac (HOL_ss addsimps [fst_conv, snd_conv]));