# HG changeset patch
# User bulwahn
# Date 1300102452 -3600
# Node ID d65835c381dd9c4f848519606b2d25e87f3ab8c5
# Parent  328371f4f927b2a708167e7610ba99bb04dcd23e
tuned exhaustive_generators

diff -r 328371f4f927 -r d65835c381dd src/HOL/Tools/Quickcheck/exhaustive_generators.ML
--- 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