# HG changeset patch
# User bulwahn
# Date 1299853273 -3600
# Node ID 9792a882da9c6aa7979d475c1afa349f71bbf2fc
# Parent  d786a8a3dc47ee5b186c7d055394c7d05b85f011
renaming tester from lazy_exhaustive to narrowing

diff -r d786a8a3dc47 -r 9792a882da9c src/HOL/Tools/Quickcheck/narrowing_generators.ML
--- 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