# HG changeset patch
# User bulwahn
# Date 1291362047 -3600
# Node ID 508c838273647e7e7feaea182cebb4de077bb978
# Parent  e006d1e069207f5172a56a36b1b079a63a8901f7
removed dead test_term_small function in quickcheck

diff -r e006d1e06920 -r 508c83827364 src/Tools/quickcheck.ML
--- a/src/Tools/quickcheck.ML	Fri Dec 03 08:40:47 2010 +0100
+++ b/src/Tools/quickcheck.ML	Fri Dec 03 08:40:47 2010 +0100
@@ -173,35 +173,6 @@
     val time = Time.toMilliseconds (#cpu (end_timing start))
   in (Exn.release result, (description, time)) end
 
-fun test_term_small ctxt t =
-  let
-    val (names, t') = prep_test_term t;
-    val current_size = Unsynchronized.ref 0
-    fun excipit s =
-      "Quickcheck " ^ s ^ " while testing at size " ^ string_of_int (!current_size)
-    val (tester, comp_time) = cpu_time "compilation"
-      (fn () => the (AList.lookup (op =) ((fst o Data.get o Context.Proof) ctxt) "small") ctxt t');
-    val empty_report = Report { iterations = 0, raised_match_errors = 0,
-      satisfied_assms = [], positive_concl_tests = 0 }
-    fun with_size k timings =
-      if k > Config.get ctxt size then (NONE, timings)
-      else
-        let
-          val _ = if Config.get ctxt quiet then () else Output.urgent_message ("Test data size: " ^ string_of_int k);
-          val _ = current_size := k
-          val (result, timing) = cpu_time ("size " ^ string_of_int k)
-            (fn () => (fst (tester k)) handle Match => (if Config.get ctxt quiet then ()
-              else warning "Exception Match raised during quickcheck"; NONE))
-        in
-          case result of
-            NONE => with_size (k + 1) (timing :: timings)
-          | SOME q => (SOME q, (timing :: timings))
-        end;
-     val result = with_size 1 [comp_time]
-   in
-     apsnd (rpair NONE) (apfst (Option.map (curry (op ~~) names)) result)
-   end
-
 (* we actually assume we know the generators and its behaviour *)
 fun is_iteratable "SML" = true
   | is_iteratable "random" = true