--- a/src/HOL/Tools/Quickcheck/exhaustive_generators.ML Thu Dec 01 22:14:35 2011 +0100
+++ b/src/HOL/Tools/Quickcheck/exhaustive_generators.ML Thu Dec 01 22:14:35 2011 +0100
@@ -489,8 +489,7 @@
thy (SOME target) (K I) (HOLogic.mk_list @{typ "code_numeral => bool"} ts') []
end;
-val test_goals = Quickcheck_Common.generator_test_goal_terms ("exhaustive",
- apfst (Option.map snd) ooo compile_generator_expr);
+val test_goals = Quickcheck_Common.generator_test_goal_terms ("exhaustive", compile_generator_expr);
(* setup *)