1signature term_pp = 2sig 3 4 type term = Term.term 5 val pp_term : 6 term_grammar.grammar -> type_grammar.grammar -> PPBackEnd.t -> 7 term -> term_pp_types.uprinter 8 9 10 (* this initialises a reference storing a function for pulling apart 11 case splits. It's expected that the initialisation will be called 12 from inside the TypeBase *) 13 val init_casesplit_munger : (term -> term * (term * term) list) -> unit 14 15end 16