# HG changeset patch
# User bulwahn
# Date 1342514379 -7200
# Node ID 65233084e9d701dc6ea20d72c76642ad52aafea0
# Parent  db75b4005d9aa2bcd90296795ea6a0baa28a160d
improved equality optimisation in Quickcheck

diff -r db75b4005d9a -r 65233084e9d7 src/HOL/Quickcheck.thy
--- a/src/HOL/Quickcheck.thy	Mon Jul 16 21:20:56 2012 +0200
+++ b/src/HOL/Quickcheck.thy	Tue Jul 17 10:39:39 2012 +0200
@@ -19,7 +19,7 @@
 axiomatization catch_match :: "'a => 'a => 'a"
 
 code_const catch_match 
-  (Quickcheck "(_) handle Match => _")
+  (Quickcheck "((_) handle Match => _)")
 
 subsection {* The @{text random} class *}
 
diff -r db75b4005d9a -r 65233084e9d7 src/HOL/Tools/Quickcheck/exhaustive_generators.ML
--- 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)])