# HG changeset patch
# User wenzelm
# Date 1294951813 -3600
# Node ID 414a68d72279f9471be06ced3c34ad4e655dc4a7
# Parent  0e02dd4f87f0ee3913d3ab54b994d11b066ea6c8
more precise pretty printing -- to accomodate Scala message layout;

diff -r 0e02dd4f87f0 -r 414a68d72279 src/HOL/Tools/Function/lexicographic_order.ML
--- 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 *)