--- a/src/HOL/Quickcheck.thy Wed Aug 22 22:47:16 2012 +0200
+++ b/src/HOL/Quickcheck.thy Wed Aug 22 22:55:41 2012 +0200
@@ -4,9 +4,6 @@
theory Quickcheck
imports Random Code_Evaluation Enum
-uses
- ("Tools/Quickcheck/quickcheck_common.ML")
- ("Tools/Quickcheck/random_generators.ML")
begin
notation fcomp (infixl "\<circ>>" 60)
@@ -182,8 +179,8 @@
subsection {* Deriving random generators for datatypes *}
-use "Tools/Quickcheck/quickcheck_common.ML"
-use "Tools/Quickcheck/random_generators.ML"
+ML_file "Tools/Quickcheck/quickcheck_common.ML"
+ML_file "Tools/Quickcheck/random_generators.ML"
setup Random_Generators.setup