# HG changeset patch
# User krauss
# Date 1166018210 -3600
# Node ID 0210a5db2013040cb8c4ddc89a6eb9943e740185
# Parent  453fd9857b4c36e0cc63c5e87ac38df042720d9b
clarified error message

diff -r 453fd9857b4c -r 0210a5db2013 src/HOL/Tools/function_package/lexicographic_order.ML
--- a/src/HOL/Tools/function_package/lexicographic_order.ML	Wed Dec 13 14:54:07 2006 +0100
+++ b/src/HOL/Tools/function_package/lexicographic_order.ML	Wed Dec 13 14:56:50 2006 +0100
@@ -224,7 +224,7 @@
     val possible_order = search_table table
       in
     case possible_order of 
-        NONE => error (cat_lines ("Could not prove it by lexicographic order:"::(pr_err table thy tl base_funs)))
+        NONE => error (cat_lines ("Could not find lexicographic termination order:"::(pr_err table thy tl base_funs)))
       | SOME order  => let
       val clean_table = map (fn x => map (nth x) order) table
       val funs = map (nth base_funs) order