src/HOL/Nitpick_Examples/Manual_Nits.thy
changeset 38284 9f98107ad8b4
parent 38242 f26d590dce0f
child 38288 63425c4b5f57
--- a/src/HOL/Nitpick_Examples/Manual_Nits.thy	Mon Aug 09 12:07:59 2010 +0200
+++ b/src/HOL/Nitpick_Examples/Manual_Nits.thy	Mon Aug 09 12:40:15 2010 +0200
@@ -128,9 +128,8 @@
   | my_int_postproc _ _ _ _ t = t
 *}
 
-setup {*
-Nitpick_Model.register_term_postprocessor_global @{typ my_int}
-                                                 my_int_postproc
+declare {*
+Nitpick_Model.register_term_postprocessor @{typ my_int} my_int_postproc
 *}
 
 lemma "add x y = add x x"
@@ -213,8 +212,8 @@
 "iterates f a = LCons a (iterates f (f a))"
 sorry
 
-setup {*
-Nitpick_HOL.register_codatatype_global @{typ "'a llist"} ""
+declare {*
+Nitpick_HOL.register_codatatype @{typ "'a llist"} ""
     (map dest_Const [@{term LNil}, @{term LCons}])
 *}