src/HOL/Predicate_Compile_Examples/Predicate_Compile_Quickcheck_Examples.thy
changeset 36176 3fe7e97ccca8
parent 36040 fcd7bea01a93
child 39191 edaf5a6ffa99
--- a/src/HOL/Predicate_Compile_Examples/Predicate_Compile_Quickcheck_Examples.thy	Fri Apr 16 20:56:40 2010 +0200
+++ b/src/HOL/Predicate_Compile_Examples/Predicate_Compile_Quickcheck_Examples.thy	Fri Apr 16 21:28:09 2010 +0200
@@ -150,7 +150,7 @@
 quickcheck[generator = predicate_compile_ff_nofs, size=5, iterations=1]
 oops
 
-hide const a b
+hide_const a b
 
 subsection {* Lexicographic order *}
 (* TODO *)