--- a/src/HOL/Tools/Quickcheck/exhaustive_generators.ML Fri Mar 21 11:06:39 2014 +0100
+++ b/src/HOL/Tools/Quickcheck/exhaustive_generators.ML Fri Mar 21 11:42:32 2014 +0100
@@ -428,7 +428,7 @@
fun mk_bounded_forall_generator_expr ctxt (t, eval_terms) =
let
val frees = Term.add_free_names t []
- val dummy_term = @{term "Code_Evaluation.Const (STR ''dummy_pattern'')
+ val dummy_term = @{term "Code_Evaluation.Const (STR ''Pure.dummy_pattern'')
(Typerep.Typerep (STR ''dummy'') [])"}
val return = @{term "Some :: term list => term list option"} $
(HOLogic.mk_list @{typ "term"}