src/HOL/Quickcheck_Exhaustive.thy
changeset 58813 625d04d4fd2a
parent 58350 919149921e46
child 58826 2ed2eaabe3df
--- a/src/HOL/Quickcheck_Exhaustive.thy	Wed Oct 29 11:13:24 2014 +0100
+++ b/src/HOL/Quickcheck_Exhaustive.thy	Wed Oct 29 11:19:27 2014 +0100
@@ -618,7 +618,7 @@
 
 ML_file "Tools/Quickcheck/exhaustive_generators.ML"
 
-setup {* Exhaustive_Generators.setup *}
+setup Exhaustive_Generators.setup
 
 declare [[quickcheck_batch_tester = exhaustive]]