diff -r aaea99edc040 -r 4044a7d1720f src/HOL/Predicate_Compile_Examples/Reg_Exp_Example.thy
--- a/src/HOL/Predicate_Compile_Examples/Reg_Exp_Example.thy	Fri May 09 08:13:36 2014 +0200
+++ b/src/HOL/Predicate_Compile_Examples/Reg_Exp_Example.thy	Fri May 09 08:13:37 2014 +0200
@@ -183,7 +183,7 @@
 quickcheck[tester = smart_exhaustive]
 oops
 
-value [code] "prop_regex a_sol"
+value "prop_regex a_sol"
 
 
 end