1.1 --- a/src/HOL/Nitpick_Examples/Manual_Nits.thy	Thu Mar 11 12:22:11 2010 +0100
     1.2 +++ b/src/HOL/Nitpick_Examples/Manual_Nits.thy	Thu Mar 11 15:33:45 2010 +0100
     1.3 @@ -118,10 +118,11 @@
     1.4  oops
     1.5  
     1.6  ML {*
     1.7 -(* Proof.context -> typ -> term -> term *)
     1.8 -fun my_int_postproc _ T (Const _ $ (Const _ $ t1 $ t2)) =
     1.9 -    HOLogic.mk_number T (snd (HOLogic.dest_number t1) - snd (HOLogic.dest_number t2))
    1.10 -  | my_int_postproc _ _ t = t
    1.11 +(* Proof.context -> string -> (typ -> term list) -> typ -> term -> term *)
    1.12 +fun my_int_postproc _ _ _ T (Const _ $ (Const _ $ t1 $ t2)) =
    1.13 +    HOLogic.mk_number T (snd (HOLogic.dest_number t1)
    1.14 +                         - snd (HOLogic.dest_number t2))
    1.15 +  | my_int_postproc _ _ _ _ t = t
    1.16  *}
    1.17  
    1.18  setup {* Nitpick.register_term_postprocessor @{typ my_int} my_int_postproc *}