# HG changeset patch
# User bulwahn
# Date 1299853273 -3600
# Node ID f05fc0711bc773992ae18457b28b9f9261bce129
# Parent  fc070c5f3a4cad1c8a3d49c5564c5b9d0014173a
renaming signatures and structures; correcting header

diff -r fc070c5f3a4c -r f05fc0711bc7 src/HOL/Quickcheck.thy
--- a/src/HOL/Quickcheck.thy	Fri Mar 11 15:21:13 2011 +0100
+++ b/src/HOL/Quickcheck.thy	Fri Mar 11 15:21:13 2011 +0100
@@ -127,7 +127,7 @@
   using assms by (rule code_numeral.induct)
 
 use "Tools/Quickcheck/random_generators.ML"
-setup Quickcheck_Generators.setup
+setup Random_Generators.setup
 
 
 subsection {* Code setup *}
diff -r fc070c5f3a4c -r f05fc0711bc7 src/HOL/Tools/Quickcheck/exhaustive_generators.ML
--- a/src/HOL/Tools/Quickcheck/exhaustive_generators.ML	Fri Mar 11 15:21:13 2011 +0100
+++ b/src/HOL/Tools/Quickcheck/exhaustive_generators.ML	Fri Mar 11 15:21:13 2011 +0100
@@ -1,4 +1,4 @@
-(*  Title:      HOL/Tools/exhaustive_generators.ML
+(*  Title:      HOL/Tools/Quickcheck/exhaustive_generators.ML
     Author:     Lukas Bulwahn, TU Muenchen
 
 Exhaustive generators for various types.
diff -r fc070c5f3a4c -r f05fc0711bc7 src/HOL/Tools/Quickcheck/random_generators.ML
--- a/src/HOL/Tools/Quickcheck/random_generators.ML	Fri Mar 11 15:21:13 2011 +0100
+++ b/src/HOL/Tools/Quickcheck/random_generators.ML	Fri Mar 11 15:21:13 2011 +0100
@@ -1,10 +1,10 @@
-(*  Title:      HOL/Tools/quickcheck_generators.ML
+(*  Title:      HOL/Tools/Quickcheck/random_generators.ML
     Author:     Florian Haftmann, TU Muenchen
 
-Quickcheck generators for various types.
+Random generators for various types.
 *)
 
-signature QUICKCHECK_GENERATORS =
+signature RANDOM_GENERATORS =
 sig
   type seed = Random_Engine.seed
   val random_fun: typ -> typ -> ('a -> 'a -> bool) -> ('a -> term)
@@ -25,7 +25,7 @@
   val setup: theory -> theory
 end;
 
-structure Quickcheck_Generators : QUICKCHECK_GENERATORS =
+structure Random_Generators : RANDOM_GENERATORS =
 struct
 
 (** abstract syntax **)
@@ -424,7 +424,7 @@
       let
         val t' = mk_reporting_generator_expr thy t Ts;
         val compile = Code_Runtime.dynamic_value_strict
-          (Counterexample_Report.get, put_counterexample_report, "Quickcheck_Generators.put_counterexample_report")
+          (Counterexample_Report.get, put_counterexample_report, "Random_Generators.put_counterexample_report")
           thy (SOME target) (fn proc => fn g => fn s => g s #>> (apfst o Option.map o map) proc) t' [];
         val single_tester = compile #> Random_Engine.run
         fun iterate_and_collect size 0 report = (NONE, report)
@@ -445,7 +445,7 @@
       let
         val t' = mk_generator_expr thy t Ts;
         val compile = Code_Runtime.dynamic_value_strict
-          (Counterexample.get, put_counterexample, "Quickcheck_Generators.put_counterexample")
+          (Counterexample.get, put_counterexample, "Random_Generators.put_counterexample")
           thy (SOME target) (fn proc => fn g => fn s => g s #>> (Option.map o map) proc) t' [];
         val single_tester = compile #> Random_Engine.run
         fun iterate size 0 = NONE