diff -r 548d3f16404b -r 77aa29bf14ee src/HOL/Nitpick_Examples/Manual_Nits.thy
--- a/src/HOL/Nitpick_Examples/Manual_Nits.thy	Thu Mar 11 12:22:11 2010 +0100
+++ b/src/HOL/Nitpick_Examples/Manual_Nits.thy	Thu Mar 11 15:33:45 2010 +0100
@@ -118,10 +118,11 @@
 oops
 
 ML {*
-(* Proof.context -> 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
+(* 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 *}