--- a/src/HOL/Quickcheck_Exhaustive.thy Fri Mar 11 15:21:13 2011 +0100
+++ b/src/HOL/Quickcheck_Exhaustive.thy Fri Mar 11 15:21:13 2011 +0100
@@ -4,7 +4,7 @@
theory Quickcheck_Exhaustive
imports Quickcheck
-uses ("Tools/exhaustive_generators.ML")
+uses ("Tools/Quickcheck/exhaustive_generators.ML")
begin
subsection {* basic operations for exhaustive generators *}
@@ -366,9 +366,9 @@
[code del]: "catch_match t1 t2 = (SOME t. t = t1 \<or> t = t2)"
code_const catch_match
- (SML "(_) handle Match => _")
+ (Quickcheck "(_) handle Match => _")
-use "Tools/exhaustive_generators.ML"
+use "Tools/Quickcheck/exhaustive_generators.ML"
setup {* Exhaustive_Generators.setup *}