# HG changeset patch
# User wenzelm
# Date 1245080209 -7200
# Node ID 98a3fd346270ca54c3fcbbe6a56253b7ea8c886a
# Parent  51fb047168b7e52bc6f2ba95aac87ae0c9316633
made SML/NJ happy;

diff -r 51fb047168b7 -r 98a3fd346270 src/HOL/Tools/quickcheck_generators.ML
--- 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]));