--- a/src/HOL/Nitpick_Examples/Manual_Nits.thy Thu Mar 11 10:13:24 2010 +0100
+++ b/src/HOL/Nitpick_Examples/Manual_Nits.thy Thu Mar 11 12:22:11 2010 +0100
@@ -117,6 +117,19 @@
nitpick [show_datatypes, expect = genuine]
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
+*}
+
+setup {* Nitpick.register_term_postprocessor @{typ my_int} my_int_postproc *}
+
+lemma "add x y = add x x"
+nitpick [show_datatypes]
+oops
+
record point =
Xcoord :: int
Ycoord :: int