changeset 43876 | b8fa7287ee4c |
parent 43875 | 485d2ad43528 |
child 43877 | abd1f074cb98 |
--- a/src/HOL/Tools/Quickcheck/exhaustive_generators.ML Mon Jul 18 10:34:21 2011 +0200 +++ b/src/HOL/Tools/Quickcheck/exhaustive_generators.ML Mon Jul 18 10:34:21 2011 +0200 @@ -488,7 +488,7 @@ thy (SOME target) (K I) (HOLogic.mk_list @{typ "code_numeral => bool"} ts') [] end; -val test_goals = Quickcheck.generator_test_goal_terms; +val test_goals = Quickcheck.generator_test_goal_terms compile_generator_expr; (* setup *)