# HG changeset patch
# User krauss
# Date 1180541110 -7200
# Node ID 8e0abe0fa80f9bf72402e085d60f600def89ab61
# Parent  56ee8105c002efb445da805b40fbea549a3521a6
clarified error message

diff -r 56ee8105c002 -r 8e0abe0fa80f src/HOL/Tools/function_package/lexicographic_order.ML
--- a/src/HOL/Tools/function_package/lexicographic_order.ML	Wed May 30 02:41:26 2007 +0200
+++ b/src/HOL/Tools/function_package/lexicographic_order.ML	Wed May 30 18:05:10 2007 +0200
@@ -235,14 +235,14 @@
             val (_, _, lhs, rhs) = dest_term t 
             val prterm = string_of_cterm o (cterm_of thy)
           in (* also show prems? *)
-               i ^ ") " ^ prterm lhs ^ " '<' " ^ prterm rhs
+               i ^ ") " ^ prterm rhs ^ " ~> " ^ prterm lhs
           end
 
       val gc = map (fn i => chr (i + 96)) (1 upto length table)
       val mc = 1 upto length measure_funs
       val tstr = "   " ^ concat (map (enclose " " " " o string_of_int) mc)
                  :: map2 (fn r => fn i => i ^ ": " ^ concat (map pr_cell r)) table gc
-      val gstr = "Goals:" :: map2 pr_goal tl gc
+      val gstr = "Calls:" :: map2 pr_goal tl gc
       val mstr = "Measures:" :: map2 pr_fun measure_funs mc
       val ustr = "Unfinished subgoals:" :: pr_unprovable_subgoals table
     in