--- a/src/HOL/Tools/recdef.ML Fri Oct 02 22:15:30 2009 +0200
+++ b/src/HOL/Tools/recdef.ML Fri Oct 02 23:15:36 2009 +0200
@@ -47,11 +47,6 @@
fun map_congs f = map_hints (fn (simps, congs, wfs) => (simps, f congs, wfs));
fun map_wfs f = map_hints (fn (simps, congs, wfs) => (simps, congs, f wfs));
-fun pretty_hints ({simps, congs, wfs}: hints) =
- [Pretty.big_list "recdef simp hints:" (map Display.pretty_thm_without_context simps),
- Pretty.big_list "recdef cong hints:" (map Display.pretty_thm_without_context (map snd congs)),
- Pretty.big_list "recdef wf hints:" (map Display.pretty_thm_without_context wfs)];
-
(* congruence rules *)