src/HOL/Quickcheck_Exhaustive.thy
changeset 41920 d4fb7a418152
parent 41918 d2ab869f8b0b
child 42117 306713ec55c3
     1.1 --- a/src/HOL/Quickcheck_Exhaustive.thy	Fri Mar 11 15:21:13 2011 +0100
     1.2 +++ b/src/HOL/Quickcheck_Exhaustive.thy	Fri Mar 11 15:21:13 2011 +0100
     1.3 @@ -4,7 +4,7 @@
     1.4  
     1.5  theory Quickcheck_Exhaustive
     1.6  imports Quickcheck
     1.7 -uses ("Tools/exhaustive_generators.ML")
     1.8 +uses ("Tools/Quickcheck/exhaustive_generators.ML")
     1.9  begin
    1.10  
    1.11  subsection {* basic operations for exhaustive generators *}
    1.12 @@ -366,9 +366,9 @@
    1.13    [code del]: "catch_match t1 t2 = (SOME t. t = t1 \<or> t = t2)"
    1.14  
    1.15  code_const catch_match 
    1.16 -  (SML "(_) handle Match => _")
    1.17 +  (Quickcheck "(_) handle Match => _")
    1.18  
    1.19 -use "Tools/exhaustive_generators.ML"
    1.20 +use "Tools/Quickcheck/exhaustive_generators.ML"
    1.21  
    1.22  setup {* Exhaustive_Generators.setup *}
    1.23