diff -r f4723b1ae5a1 -r 76d8c30a92c5 src/HOL/Tools/quickcheck_generators.ML
--- a/src/HOL/Tools/quickcheck_generators.ML	Mon Jun 15 21:28:04 2009 +0200
+++ b/src/HOL/Tools/quickcheck_generators.ML	Mon Jun 15 21:33:27 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]));