diff -r 5f817bad850a -r 391913d17d15 src/HOL/Predicate_Compile_Examples/Reg_Exp_Example.thy --- a/src/HOL/Predicate_Compile_Examples/Reg_Exp_Example.thy Mon Jul 15 20:13:30 2013 +0200 +++ b/src/HOL/Predicate_Compile_Examples/Reg_Exp_Example.thy Mon Jul 15 20:36:27 2013 +0200 @@ -85,7 +85,8 @@ fun prop_regex :: "Nat * Nat * RE * RE * Sym list \ bool" where - "prop_regex (n, (k, (p, (q, s)))) = ((accepts (repInt n k (And p q)) s) = (accepts (And (repInt n k p) (repInt n k q)) s))" + "prop_regex (n, (k, (p, (q, s)))) = + ((accepts (repInt n k (And p q)) s) = (accepts (And (repInt n k p) (repInt n k q)) s))" @@ -97,7 +98,10 @@ oops -setup {* Context.theory_map (Quickcheck.add_tester ("prolog", (Code_Prolog.active, Code_Prolog.test_goals))) *} +setup {* + Context.theory_map + (Quickcheck.add_tester ("prolog", (Code_Prolog.active, Code_Prolog.test_goals))) +*} setup {* Code_Prolog.map_code_options (K {ensure_groundness = true,