src/HOL/Tools/Nitpick/nitpick_model.ML
changeset 38284 9f98107ad8b4
parent 38240 a44d108a8d39
child 38864 4abe644fcea5
     1.1 --- a/src/HOL/Tools/Nitpick/nitpick_model.ML	Mon Aug 09 12:07:59 2010 +0200
     1.2 +++ b/src/HOL/Tools/Nitpick/nitpick_model.ML	Mon Aug 09 12:40:15 2010 +0200
     1.3 @@ -25,10 +25,11 @@
     1.4    val unknown : string
     1.5    val unrep : unit -> string
     1.6    val register_term_postprocessor :
     1.7 -    typ -> term_postprocessor -> Proof.context -> Proof.context
     1.8 +    typ -> term_postprocessor -> morphism -> Context.generic -> Context.generic
     1.9    val register_term_postprocessor_global :
    1.10      typ -> term_postprocessor -> theory -> theory
    1.11 -  val unregister_term_postprocessor : typ -> Proof.context -> Proof.context
    1.12 +  val unregister_term_postprocessor :
    1.13 +    typ -> morphism -> Context.generic -> Context.generic
    1.14    val unregister_term_postprocessor_global : typ -> theory -> theory
    1.15    val tuple_list_for_name :
    1.16      nut NameTable.table -> Kodkod.raw_bound list -> nut -> int list list
    1.17 @@ -158,15 +159,18 @@
    1.18                | ord => ord)
    1.19             | _ => Term_Ord.fast_term_ord tp
    1.20  
    1.21 -fun register_term_postprocessor_generic T p = Data.map (cons (T, p))
    1.22 -val register_term_postprocessor =
    1.23 -  Context.proof_map oo register_term_postprocessor_generic
    1.24 +fun register_term_postprocessor_generic T postproc =
    1.25 +  Data.map (cons (T, postproc))
    1.26 +(* TODO: Consider morphism. *)
    1.27 +fun register_term_postprocessor T postproc (_ : morphism) =
    1.28 +  register_term_postprocessor_generic T postproc
    1.29  val register_term_postprocessor_global =
    1.30    Context.theory_map oo register_term_postprocessor_generic
    1.31  
    1.32  fun unregister_term_postprocessor_generic T = Data.map (AList.delete (op =) T)
    1.33 -val unregister_term_postprocessor =
    1.34 -  Context.proof_map o unregister_term_postprocessor_generic
    1.35 +(* TODO: Consider morphism. *)
    1.36 +fun unregister_term_postprocessor T (_ : morphism) =
    1.37 +  unregister_term_postprocessor_generic T
    1.38  val unregister_term_postprocessor_global =
    1.39    Context.theory_map o unregister_term_postprocessor_generic
    1.40