46 fun map_simps f = map_hints (fn (simps, congs, wfs) => (f simps, congs, wfs)); |
46 fun map_simps f = map_hints (fn (simps, congs, wfs) => (f simps, congs, wfs)); |
47 fun map_congs f = map_hints (fn (simps, congs, wfs) => (simps, f congs, wfs)); |
47 fun map_congs f = map_hints (fn (simps, congs, wfs) => (simps, f congs, wfs)); |
48 fun map_wfs f = map_hints (fn (simps, congs, wfs) => (simps, congs, f wfs)); |
48 fun map_wfs f = map_hints (fn (simps, congs, wfs) => (simps, congs, f wfs)); |
49 |
49 |
50 fun pretty_hints ({simps, congs, wfs}: hints) = |
50 fun pretty_hints ({simps, congs, wfs}: hints) = |
51 [Pretty.big_list "recdef simp hints:" (map Display.pretty_thm simps), |
51 [Pretty.big_list "recdef simp hints:" (map Display.pretty_thm_without_context simps), |
52 Pretty.big_list "recdef cong hints:" (map Display.pretty_thm (map snd congs)), |
52 Pretty.big_list "recdef cong hints:" (map Display.pretty_thm_without_context (map snd congs)), |
53 Pretty.big_list "recdef wf hints:" (map Display.pretty_thm wfs)]; |
53 Pretty.big_list "recdef wf hints:" (map Display.pretty_thm_without_context wfs)]; |
54 |
54 |
55 |
55 |
56 (* congruence rules *) |
56 (* congruence rules *) |
57 |
57 |
58 local |
58 local |