1.1 --- a/src/Tools/quickcheck.ML	Wed Apr 20 14:43:04 2011 +0200
     1.2 +++ b/src/Tools/quickcheck.ML	Wed Apr 20 16:00:44 2011 +0200
     1.3 @@ -507,10 +507,14 @@
     1.4      maps (fn (label, time) =>
     1.5        Pretty.str (label ^ ": " ^ string_of_int time ^ " ms") :: Pretty.brk 1 :: []) (rev timings))
     1.6  
     1.7 -fun pretty_counterex_and_reports ctxt auto (result :: _) =
     1.8 -  Pretty.chunks (pretty_counterex ctxt auto (response_of result) ::
     1.9 -    (* map (pretty_reports ctxt) (reports_of result) :: *)
    1.10 -    (if Config.get ctxt timing then cons (pretty_timings (timings_of result)) else I) [])
    1.11 +fun pretty_counterex_and_reports ctxt auto [] =
    1.12 +    Pretty.chunks [Pretty.strs (tool_name auto ::
    1.13 +        space_explode " " "is used in a locale where no interpretation is provided."),
    1.14 +      Pretty.strs (space_explode " " "Please provide an executable interpretation for the locale.")]
    1.15 +  | pretty_counterex_and_reports ctxt auto (result :: _) =
    1.16 +    Pretty.chunks (pretty_counterex ctxt auto (response_of result) ::
    1.17 +      (* map (pretty_reports ctxt) (reports_of result) :: *)
    1.18 +      (if Config.get ctxt timing then cons (pretty_timings (timings_of result)) else I) [])
    1.19  
    1.20  (* automatic testing *)
    1.21  
    1.22 @@ -593,11 +597,11 @@
    1.23  fun quickcheck_params_cmd args = Context.theory_map (fold parse_test_param args);
    1.24  
    1.25  fun check_expectation state results =
    1.26 -  (if found_counterexample (hd results) andalso expect (Proof.context_of state) = No_Counterexample
    1.27 +  (if exists found_counterexample results andalso expect (Proof.context_of state) = No_Counterexample
    1.28    then
    1.29      error ("quickcheck expected to find no counterexample but found one")
    1.30    else
    1.31 -    (if not (found_counterexample (hd results)) andalso expect (Proof.context_of state) = Counterexample
    1.32 +    (if not (exists found_counterexample results) andalso expect (Proof.context_of state) = Counterexample
    1.33      then
    1.34        error ("quickcheck expected to find a counterexample but did not find one")
    1.35      else ()))