src/HOL/Tools/Quickcheck/quickcheck_common.ML
changeset 44241 7943b69f0188
parent 42793 88bee9f6eec7
child 45039 632a033616e9
--- a/src/HOL/Tools/Quickcheck/quickcheck_common.ML	Wed Aug 17 16:46:58 2011 +0200
+++ b/src/HOL/Tools/Quickcheck/quickcheck_common.ML	Wed Aug 17 18:05:31 2011 +0200
@@ -112,7 +112,7 @@
       if_t $ (HOLogic.eq_const @{typ code_numeral} $ Bound 0 $ HOLogic.mk_number @{typ code_numeral} index) $
         (mk_generator_expr ctxt (t, eval_terms)) $ else_t
   in
-    absdummy (@{typ "code_numeral"}, fold_rev mk_if (1 upto (length ts) ~~ ts) out_of_bounds)
+    absdummy @{typ "code_numeral"} (fold_rev mk_if (1 upto (length ts) ~~ ts) out_of_bounds)
   end
 
 (** post-processing of function terms **)