handling the case where quickcheck is used in a locale with no known interpretation user-friendly

--- a/src/Tools/quickcheck.ML	Wed Apr 20 14:43:04 2011 +0200
+++ b/src/Tools/quickcheck.ML	Wed Apr 20 16:00:44 2011 +0200
@@ -507,10 +507,14 @@
     maps (fn (label, time) =>
       Pretty.str (label ^ ": " ^ string_of_int time ^ " ms") :: Pretty.brk 1 :: []) (rev timings))
 
-fun pretty_counterex_and_reports ctxt auto (result :: _) =
-  Pretty.chunks (pretty_counterex ctxt auto (response_of result) ::
-    (* map (pretty_reports ctxt) (reports_of result) :: *)
-    (if Config.get ctxt timing then cons (pretty_timings (timings_of result)) else I) [])
+fun pretty_counterex_and_reports ctxt auto [] =
+    Pretty.chunks [Pretty.strs (tool_name auto ::
+        space_explode " " "is used in a locale where no interpretation is provided."),
+      Pretty.strs (space_explode " " "Please provide an executable interpretation for the locale.")]
+  | pretty_counterex_and_reports ctxt auto (result :: _) =
+    Pretty.chunks (pretty_counterex ctxt auto (response_of result) ::
+      (* map (pretty_reports ctxt) (reports_of result) :: *)
+      (if Config.get ctxt timing then cons (pretty_timings (timings_of result)) else I) [])
 
 (* automatic testing *)
 
@@ -593,11 +597,11 @@
 fun quickcheck_params_cmd args = Context.theory_map (fold parse_test_param args);
 
 fun check_expectation state results =
-  (if found_counterexample (hd results) andalso expect (Proof.context_of state) = No_Counterexample
+  (if exists found_counterexample results andalso expect (Proof.context_of state) = No_Counterexample
   then
     error ("quickcheck expected to find no counterexample but found one")
   else
-    (if not (found_counterexample (hd results)) andalso expect (Proof.context_of state) = Counterexample
+    (if not (exists found_counterexample results) andalso expect (Proof.context_of state) = Counterexample
     then
       error ("quickcheck expected to find a counterexample but did not find one")
     else ()))