diff -r 842057125043 -r f26d590dce0f src/HOL/Nitpick_Examples/Manual_Nits.thy
--- a/src/HOL/Nitpick_Examples/Manual_Nits.thy	Fri Aug 06 17:18:29 2010 +0200
+++ b/src/HOL/Nitpick_Examples/Manual_Nits.thy	Fri Aug 06 17:23:11 2010 +0200
@@ -122,14 +122,16 @@
 oops
 
 ML {*
-(* Proof.context -> string -> (typ -> term list) -> typ -> term -> term *)
 fun my_int_postproc _ _ _ T (Const _ $ (Const _ $ t1 $ t2)) =
     HOLogic.mk_number T (snd (HOLogic.dest_number t1)
                          - snd (HOLogic.dest_number t2))
   | my_int_postproc _ _ _ _ t = t
 *}
 
-setup {* Nitpick.register_term_postprocessor @{typ my_int} my_int_postproc *}
+setup {*
+Nitpick_Model.register_term_postprocessor_global @{typ my_int}
+                                                 my_int_postproc
+*}
 
 lemma "add x y = add x x"
 nitpick [show_datatypes]
@@ -212,7 +214,7 @@
 sorry
 
 setup {*
-Nitpick.register_codatatype @{typ "'a llist"} ""
+Nitpick_HOL.register_codatatype_global @{typ "'a llist"} ""
     (map dest_Const [@{term LNil}, @{term LCons}])
 *}