tuned
authorhaftmann
Fri, 10 Jul 2009 07:59:23 +0200
changeset 31984 97d6472dd302
parent 31968 0314441a53a6
child 31985 a6e982b1ebba
tuned
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;