--- a/src/HOL/Tools/Function/lexicographic_order.ML Thu Jan 13 20:54:07 2011 +0100
+++ b/src/HOL/Tools/Function/lexicographic_order.ML Thu Jan 13 21:50:13 2011 +0100
@@ -198,8 +198,11 @@
let
val clean_table = map (fn x => map (nth x) order) table
val relation = mk_measures domT (map (nth measure_funs) order)
- val _ = if not quiet
- then writeln ("Found termination order: " ^ quote (Syntax.string_of_term ctxt relation))
+ val _ =
+ if not quiet then
+ Pretty.writeln (Pretty.block
+ [Pretty.str "Found termination order:", Pretty.brk 1,
+ Pretty.quote (Syntax.pretty_term ctxt relation)])
else ()
in (* 4: proof reconstruction *)