--- a/src/HOL/Nitpick_Examples/Manual_Nits.thy Mon Aug 09 12:53:16 2010 +0200
+++ b/src/HOL/Nitpick_Examples/Manual_Nits.thy Mon Aug 09 13:46:25 2010 +0200
@@ -128,7 +128,7 @@
| my_int_postproc _ _ _ _ t = t
*}
-declare {*
+declaration {*
Nitpick_Model.register_term_postprocessor @{typ my_int} my_int_postproc
*}
@@ -212,7 +212,7 @@
"iterates f a = LCons a (iterates f (f a))"
sorry
-declare {*
+declaration {*
Nitpick_HOL.register_codatatype @{typ "'a llist"} ""
(map dest_Const [@{term LNil}, @{term LCons}])
*}