--- 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 *}