src/HOL/Tools/recdef.ML
changeset 32863 5e8cef567042
parent 32149 ef59550a55d3
child 32952 aeb1e44fbc19
--- 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 *)