# HG changeset patch
# User haftmann
# Date 1247205563 -7200
# Node ID 97d6472dd3024955a39c9d1c0bee2a702290ff92
# Parent  0314441a53a6eff9ef4ece0d6ebcbe19301fdd07
tuned

diff -r 0314441a53a6 -r 97d6472dd302 src/HOL/Tools/quickcheck_generators.ML
--- a/src/HOL/Tools/quickcheck_generators.ML	Thu Jul 09 10:34:51 2009 +0200
+++ b/src/HOL/Tools/quickcheck_generators.ML	Fri Jul 10 07:59:23 2009 +0200
@@ -27,7 +27,7 @@
 
 fun termifyT T = HOLogic.mk_prodT (T, @{typ "unit => term"})
 val size = @{term "i::code_numeral"};
-val size1 = @{term "(i::code_numeral) - 1"};
+val size_pred = @{term "(i::code_numeral) - 1"};
 val size' = @{term "j::code_numeral"};
 val seed = @{term "s::Random.seed"};
 
@@ -243,7 +243,7 @@
           | mk_random_fun_lift (fT :: fTs) t =
               mk_const @{const_name random_fun_lift} [fTs ---> T, fT] $
                 mk_random_fun_lift fTs t;
-        val t = mk_random_fun_lift fTs (nth random_auxs k $ size1 $ size');
+        val t = mk_random_fun_lift fTs (nth random_auxs k $ size_pred $ size');
         val size = Option.map snd (DatatypeCodegen.find_shortest_path descr k)
           |> the_default 0;
       in (SOME size, (t, fTs ---> T)) end;