changeset 45420 | d17556b9a89b |
parent 45159 | 3f1d1ce024cb |
child 45484 | 23871e17dddb |
--- a/src/HOL/Tools/Quickcheck/exhaustive_generators.ML Wed Nov 09 11:34:59 2011 +0100 +++ b/src/HOL/Tools/Quickcheck/exhaustive_generators.ML Wed Nov 09 11:35:09 2011 +0100 @@ -488,7 +488,7 @@ thy (SOME target) (K I) (HOLogic.mk_list @{typ "code_numeral => bool"} ts') [] end; -val test_goals = Quickcheck_Common.generator_test_goal_terms compile_generator_expr; +val test_goals = Quickcheck_Common.generator_test_goal_terms ("exhaustive", compile_generator_expr); (* setup *)