# HG changeset patch
# User blanchet
# Date 1303311769 -7200
# Node ID 4344b3654961236bc24487f18b820fee716c7343
# Parent  c3d880b13aa9eb6386775760d8fcdfca8950be1a# Parent  0f60055d10fb3830d403160577daf25c3dbff549
merged

diff -r 0f60055d10fb -r 4344b3654961 src/HOL/Mutabelle/mutabelle_extra.ML
--- a/src/HOL/Mutabelle/mutabelle_extra.ML	Wed Apr 20 16:49:21 2011 +0200
+++ b/src/HOL/Mutabelle/mutabelle_extra.ML	Wed Apr 20 17:02:49 2011 +0200
@@ -273,7 +273,9 @@
  @{const_name "ord_fun_inst.less_fun"},
  @{const_name Metis.fequal},
  @{const_name Meson.skolem},
- @{const_name transfer_morphism}
+ @{const_name transfer_morphism},
+ @{const_name enum_prod_inst.enum_all_prod},
+ @{const_name enum_prod_inst.enum_ex_prod}
  (*@{const_name "==>"}, @{const_name "=="}*)]
 
 val forbidden_mutant_consts =
diff -r 0f60055d10fb -r 4344b3654961 src/HOL/ex/Quickcheck_Examples.thy
--- a/src/HOL/ex/Quickcheck_Examples.thy	Wed Apr 20 16:49:21 2011 +0200
+++ b/src/HOL/ex/Quickcheck_Examples.thy	Wed Apr 20 17:02:49 2011 +0200
@@ -294,4 +294,28 @@
 quickcheck[random, size = 10]
 oops
 
+subsection {* Examples with locales *}
+
+locale Truth
+
+context Truth
+begin
+
+lemma "False"
+quickcheck[expect = no_counterexample]
+oops
+
 end
+
+interpretation Truth .
+
+context Truth
+begin
+
+lemma "False"
+quickcheck[expect = counterexample]
+oops
+
+end
+
+end
diff -r 0f60055d10fb -r 4344b3654961 src/Tools/quickcheck.ML
--- a/src/Tools/quickcheck.ML	Wed Apr 20 16:49:21 2011 +0200
+++ b/src/Tools/quickcheck.ML	Wed Apr 20 17:02:49 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 ()))