1.1 --- a/src/HOL/Nitpick_Examples/Manual_Nits.thy	Thu Mar 11 10:13:24 2010 +0100
     1.2 +++ b/src/HOL/Nitpick_Examples/Manual_Nits.thy	Thu Mar 11 12:22:11 2010 +0100
     1.3 @@ -117,6 +117,19 @@
     1.4  nitpick [show_datatypes, expect = genuine]
     1.5  oops
     1.6  
     1.7 +ML {*
     1.8 +(* Proof.context -> typ -> term -> term *)
     1.9 +fun my_int_postproc _ T (Const _ $ (Const _ $ t1 $ t2)) =
    1.10 +    HOLogic.mk_number T (snd (HOLogic.dest_number t1) - snd (HOLogic.dest_number t2))
    1.11 +  | my_int_postproc _ _ t = t
    1.12 +*}
    1.13 +
    1.14 +setup {* Nitpick.register_term_postprocessor @{typ my_int} my_int_postproc *}
    1.15 +
    1.16 +lemma "add x y = add x x"
    1.17 +nitpick [show_datatypes]
    1.18 +oops
    1.19 +
    1.20  record point =
    1.21    Xcoord :: int
    1.22    Ycoord :: int