--- a/src/HOL/Predicate_Compile_Examples/Reg_Exp_Example.thy Thu Sep 16 13:49:06 2010 +0200
+++ b/src/HOL/Predicate_Compile_Examples/Reg_Exp_Example.thy Thu Sep 16 13:49:08 2010 +0200
@@ -96,7 +96,7 @@
oops
-setup {* Quickcheck.add_generator ("prolog", Code_Prolog.quickcheck) *}
+setup {* Context.theory_map (Quickcheck.add_generator ("prolog", Code_Prolog.quickcheck)) *}
setup {* Code_Prolog.map_code_options (K
{ensure_groundness = true,
@@ -108,9 +108,7 @@
(("subP", "limited_subP"), "repIntP"),
(("repIntPa", "limited_repIntPa"), "repIntP"),
(("accepts", "limited_accepts"), "quickcheck")],
- manual_reorder = [],
- timeout = Time.fromSeconds 10,
- prolog_system = Code_Prolog.SWI_PROLOG}) *}
+ manual_reorder = []}) *}
text {* Finding the counterexample still seems out of reach for the
prolog-style generation. *}