--- a/src/HOL/Tools/Quickcheck/narrowing_generators.ML Fri Mar 11 15:21:13 2011 +0100
+++ b/src/HOL/Tools/Quickcheck/narrowing_generators.ML Fri Mar 11 15:21:13 2011 +0100
@@ -79,7 +79,7 @@
structure Counterexample = Proof_Data
(
type T = unit -> term list option
- fun init _ () = error " Quickcheck_Narrowing_Result"
+ fun init _ () = error "Counterexample"
)
val put_counterexample = Counterexample.put
@@ -99,6 +99,6 @@
val setup =
Context.theory_map
- (Quickcheck.add_generator ("lazy_exhaustive", compile_generator_expr))
+ (Quickcheck.add_generator ("narrowing", compile_generator_expr))
end;
\ No newline at end of file