1.1 --- a/src/Tools/quickcheck.ML	Thu Apr 19 08:45:13 2012 +0200
     1.2 +++ b/src/Tools/quickcheck.ML	Thu Apr 19 10:16:51 2012 +0200
     1.3 @@ -137,14 +137,6 @@
     1.4    | set_response _ _ NONE result = result
     1.5  
     1.6  
     1.7 -fun set_counterexample counterexample (Result r) =
     1.8 -  Result {counterexample = counterexample,  evaluation_terms = #evaluation_terms r,
     1.9 -    timings = #timings r, reports = #reports r}
    1.10 -
    1.11 -fun set_evaluation_terms evaluation_terms (Result r) =
    1.12 -  Result {counterexample = #counterexample r,  evaluation_terms = evaluation_terms,
    1.13 -    timings = #timings r, reports = #reports r}
    1.14 -
    1.15  fun cons_timing timing (Result r) =
    1.16    Result {counterexample = #counterexample r, evaluation_terms = #evaluation_terms r,
    1.17      timings = cons timing (#timings r), reports = #reports r}
    1.18 @@ -288,8 +280,6 @@
    1.19  val mk_batch_validator =
    1.20    gen_mk_tester (fn ctxt => AList.lookup (op =) ((snd o snd o fst o Data.get o Context.Proof) ctxt))
    1.21    
    1.22 -fun lookup_tester ctxt = AList.lookup (op =) ((fst o fst o Data.get o Context.Proof) ctxt)
    1.23 -
    1.24  (* testing propositions *)
    1.25  
    1.26  type compile_generator =
    1.27 @@ -413,27 +403,11 @@
    1.28       @ [pretty_stat "positive conclusion tests" positive_concl_tests])
    1.29    end
    1.30  
    1.31 -fun pretty_reports ctxt (SOME reports) =
    1.32 -  Pretty.chunks (Pretty.fbrk :: Pretty.str "Quickcheck report:" ::
    1.33 -    maps (fn (size, report) =>
    1.34 -      Pretty.str ("size " ^ string_of_int size ^ ":") :: pretty_report report @ [Pretty.brk 1])
    1.35 -      (rev reports))
    1.36 -  | pretty_reports ctxt NONE = Pretty.str ""
    1.37 -
    1.38  fun pretty_timings timings =
    1.39    Pretty.chunks (Pretty.fbrk :: Pretty.str "timings:" ::
    1.40      maps (fn (label, time) =>
    1.41        Pretty.str (label ^ ": " ^ string_of_int time ^ " ms") :: Pretty.brk 1 :: []) (rev timings))
    1.42  
    1.43 -fun pretty_counterex_and_reports ctxt auto [] =
    1.44 -    Pretty.chunks [Pretty.strs (tool_name auto ::
    1.45 -        space_explode " " "is used in a locale where no interpretation is provided."),
    1.46 -      Pretty.strs (space_explode " " "Please provide an executable interpretation for the locale.")]
    1.47 -  | pretty_counterex_and_reports ctxt auto (result :: _) =
    1.48 -    Pretty.chunks (pretty_counterex ctxt auto (response_of result) ::
    1.49 -      (* map (pretty_reports ctxt) (reports_of result) :: *)
    1.50 -      (if Config.get ctxt timing then cons (pretty_timings (timings_of result)) else I) [])
    1.51 -
    1.52  (* Isar commands *)
    1.53  
    1.54  fun read_nat s = case (Library.read_int o Symbol.explode) s