# HG changeset patch
# User bulwahn
# Date 1301552883 -7200
# Node ID 5cb4a2f4f2a40fa15598a2f58c2138996b3778bf
# Parent  c7b6d8d9922edfcf9eaf0cade9f0af5569895ba9# Parent  d0be2722ce9f360a582df76003bc084268f056e0
merged

diff -r d0be2722ce9f -r 5cb4a2f4f2a4 src/HOL/Quickcheck.thy
--- a/src/HOL/Quickcheck.thy	Wed Mar 30 23:26:40 2011 +0200
+++ b/src/HOL/Quickcheck.thy	Thu Mar 31 08:28:03 2011 +0200
@@ -209,12 +209,5 @@
 hide_type (open) randompred
 hide_const (open) random collapse beyond random_fun_aux random_fun_lift
   iter' iter empty single bind union if_randompred iterate_upto not_randompred Random map
-declare [[quickcheck_timing]]
-lemma
-  "rev xs = xs"
-quickcheck[tester = random, finite_types = true, report = false]
-
-quickcheck[tester = random, finite_types = false, report = false]
-oops
 
 end
diff -r d0be2722ce9f -r 5cb4a2f4f2a4 src/HOL/Tools/Quickcheck/exhaustive_generators.ML
--- a/src/HOL/Tools/Quickcheck/exhaustive_generators.ML	Wed Mar 30 23:26:40 2011 +0200
+++ b/src/HOL/Tools/Quickcheck/exhaustive_generators.ML	Thu Mar 31 08:28:03 2011 +0200
@@ -287,20 +287,6 @@
 val put_counterexample_batch = Counterexample_Batch.put;
 
 val target = "Quickcheck";
-(*
-fun compile_simple_generator_expr ctxt (t, eval_terms) =
-  let
-    val thy = ProofContext.theory_of ctxt
-    val t' = mk_generator_expr ctxt (t, eval_terms);
-    val compile = Code_Runtime.dynamic_value_strict
-      (Counterexample.get, put_counterexample, "Exhaustive_Generators.put_counterexample")
-      thy (SOME target) (fn proc => fn g => g #> (Option.map o map) proc) t' [];
-  in
-    fn [size] => rpair NONE (compile [size] |> 
-      (if Config.get ctxt quickcheck_pretty then
-        Option.map (map Quickcheck_Common.post_process_term) else I))
-  end;
-*)
   
 fun compile_generator_expr ctxt ts =
   let