# HG changeset patch
# User wenzelm
# Date 1414577967 -3600
# Node ID 625d04d4fd2a1fd83afeff38dc66a442ae456ee4
# Parent  5a9a2d3b9f8b5b7ddae8c7d2c563911a41087b68
tuned;

diff -r 5a9a2d3b9f8b -r 625d04d4fd2a src/HOL/Quickcheck_Benchmark/Needham_Schroeder_Base.thy
--- a/src/HOL/Quickcheck_Benchmark/Needham_Schroeder_Base.thy	Wed Oct 29 11:13:24 2014 +0100
+++ b/src/HOL/Quickcheck_Benchmark/Needham_Schroeder_Base.thy	Wed Oct 29 11:19:27 2014 +0100
@@ -194,7 +194,7 @@
 declare ListMem_iff[symmetric, code_pred_inline]
 declare [[quickcheck_timing]]
 
-setup {* Exhaustive_Generators.setup_exhaustive_datatype_interpretation *}
+setup Exhaustive_Generators.setup_exhaustive_datatype_interpretation
 declare [[quickcheck_full_support = false]]
 
 end
\ No newline at end of file
diff -r 5a9a2d3b9f8b -r 625d04d4fd2a src/HOL/Quickcheck_Examples/Completeness.thy
--- a/src/HOL/Quickcheck_Examples/Completeness.thy	Wed Oct 29 11:13:24 2014 +0100
+++ b/src/HOL/Quickcheck_Examples/Completeness.thy	Wed Oct 29 11:19:27 2014 +0100
@@ -20,7 +20,7 @@
   "is_some x \<longleftrightarrow> x \<noteq> None"
   by (cases x) simp_all
 
-setup {* Exhaustive_Generators.setup_exhaustive_datatype_interpretation *} 
+setup Exhaustive_Generators.setup_exhaustive_datatype_interpretation
 
 subsection {* Defining the size of values *}
 
diff -r 5a9a2d3b9f8b -r 625d04d4fd2a src/HOL/Quickcheck_Examples/Quickcheck_Examples.thy
--- a/src/HOL/Quickcheck_Examples/Quickcheck_Examples.thy	Wed Oct 29 11:13:24 2014 +0100
+++ b/src/HOL/Quickcheck_Examples/Quickcheck_Examples.thy	Wed Oct 29 11:19:27 2014 +0100
@@ -544,7 +544,7 @@
 
 text {* with the simple testing scheme *}
 
-setup {* Exhaustive_Generators.setup_exhaustive_datatype_interpretation *}
+setup Exhaustive_Generators.setup_exhaustive_datatype_interpretation
 declare [[quickcheck_full_support = false]]
 
 lemma
diff -r 5a9a2d3b9f8b -r 625d04d4fd2a src/HOL/Quickcheck_Examples/Quickcheck_Interfaces.thy
--- a/src/HOL/Quickcheck_Examples/Quickcheck_Interfaces.thy	Wed Oct 29 11:13:24 2014 +0100
+++ b/src/HOL/Quickcheck_Examples/Quickcheck_Interfaces.thy	Wed Oct 29 11:19:27 2014 +0100
@@ -11,7 +11,7 @@
 First, this requires to setup special generators for all datatypes via the following command.
 *}
 
-setup {* Exhaustive_Generators.setup_bounded_forall_datatype_interpretation *}
+setup Exhaustive_Generators.setup_bounded_forall_datatype_interpretation
 
 text {*
 Now, the function Quickcheck.mk_batch_validator : Proof.context -> term list -> (int -> bool) list option
diff -r 5a9a2d3b9f8b -r 625d04d4fd2a src/HOL/Quickcheck_Exhaustive.thy
--- 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]]
 
diff -r 5a9a2d3b9f8b -r 625d04d4fd2a src/HOL/Quickcheck_Narrowing.thy
--- a/src/HOL/Quickcheck_Narrowing.thy	Wed Oct 29 11:13:24 2014 +0100
+++ b/src/HOL/Quickcheck_Narrowing.thy	Wed Oct 29 11:19:27 2014 +0100
@@ -197,7 +197,7 @@
 
 ML_file "Tools/Quickcheck/narrowing_generators.ML"
 
-setup {* Narrowing_Generators.setup *}
+setup Narrowing_Generators.setup
 
 definition narrowing_dummy_partial_term_of :: "('a :: partial_term_of) itself => narrowing_term => term"
 where