1.1 --- a/src/HOL/Tools/Nitpick/nitpick.ML	Thu Mar 11 10:13:24 2010 +0100
     1.2 +++ b/src/HOL/Tools/Nitpick/nitpick.ML	Thu Mar 11 12:22:11 2010 +0100
     1.3 @@ -8,6 +8,7 @@
     1.4  signature NITPICK =
     1.5  sig
     1.6    type styp = Nitpick_Util.styp
     1.7 +  type term_postprocessor = Nitpick_Model.term_postprocessor
     1.8    type params = {
     1.9      cards_assigns: (typ option * int list) list,
    1.10      maxes_assigns: (styp option * int list) list,
    1.11 @@ -58,6 +59,9 @@
    1.12    val unregister_frac_type : string -> theory -> theory
    1.13    val register_codatatype : typ -> string -> styp list -> theory -> theory
    1.14    val unregister_codatatype : typ -> theory -> theory
    1.15 +  val register_term_postprocessor :
    1.16 +    typ -> term_postprocessor -> theory -> theory
    1.17 +  val unregister_term_postprocessor : typ -> theory -> theory
    1.18    val pick_nits_in_term :
    1.19      Proof.state -> params -> bool -> int -> int -> int -> (term * term) list
    1.20      -> term list -> term -> string * Proof.state