src/HOL/Tools/Quickcheck/narrowing_generators.ML
changeset 41936 9792a882da9c
parent 41933 10f254a4e5b9
child 41938 645cca858c69
     1.1 --- a/src/HOL/Tools/Quickcheck/narrowing_generators.ML	Fri Mar 11 15:21:13 2011 +0100
     1.2 +++ b/src/HOL/Tools/Quickcheck/narrowing_generators.ML	Fri Mar 11 15:21:13 2011 +0100
     1.3 @@ -79,7 +79,7 @@
     1.4  structure Counterexample = Proof_Data
     1.5  (
     1.6    type T = unit -> term list option
     1.7 -  fun init _ () = error " Quickcheck_Narrowing_Result"
     1.8 +  fun init _ () = error "Counterexample"
     1.9  )
    1.10  
    1.11  val put_counterexample =  Counterexample.put
    1.12 @@ -99,6 +99,6 @@
    1.13  
    1.14  val setup =
    1.15    Context.theory_map
    1.16 -    (Quickcheck.add_generator ("lazy_exhaustive", compile_generator_expr))
    1.17 +    (Quickcheck.add_generator ("narrowing", compile_generator_expr))
    1.18      
    1.19  end;
    1.20 \ No newline at end of file