src/HOL/Tools/Quickcheck/exhaustive_generators.ML
changeset 48273 65233084e9d7
parent 48178 0192811f0a96
child 48414 43875bab3a4c
--- a/src/HOL/Tools/Quickcheck/exhaustive_generators.ML	Mon Jul 16 21:20:56 2012 +0200
+++ b/src/HOL/Tools/Quickcheck/exhaustive_generators.ML	Tue Jul 17 10:39:39 2012 +0200
@@ -332,8 +332,8 @@
                 val dummy_var = Free (singleton
                   (Variable.variant_frees ctxt (concl :: assms @ vars)) ("dummy", T))
                 val new_assms = map HOLogic.mk_eq (vars ~~ args)
-                val cont_t = mk_smart_test_term' concl (union (op =) varnames bound_vars)
-                  (new_assms @ assms) genuine
+                val bound_vars' = union (op =) (vars_of lhs) (union (op =) varnames bound_vars)
+                val cont_t = mk_smart_test_term' concl bound_vars' (new_assms @ assms) genuine
               in
                 (vars_of lhs, Datatype_Case.make_case ctxt Datatype_Case.Quiet [] lhs
                   [(list_comb (constr, vars), cont_t), (dummy_var, none_t)])