# HG changeset patch
# User wenzelm
# Date 1122916838 -7200
# Node ID abc48b981e60f7e9a51b6fe8b6267757cc90c832
# Parent  c895701d55eaf486a5a91ada52407020348bcfd3
tuned dict_ord;

diff -r c895701d55ea -r abc48b981e60 src/Pure/library.ML
--- a/src/Pure/library.ML	Mon Aug 01 19:20:37 2005 +0200
+++ b/src/Pure/library.ML	Mon Aug 01 19:20:38 2005 +0200
@@ -1144,11 +1144,11 @@
   (case a_ord (x, x') of EQUAL => b_ord (y, y') | ord => ord);
 
 (*dictionary order -- in general NOT well-founded!*)
-fun dict_ord _ ([], []) = EQUAL
+fun dict_ord elem_ord (x :: xs, y :: ys) =
+      (case elem_ord (x, y) of EQUAL => dict_ord elem_ord (xs, ys) | ord => ord)
+  | dict_ord _ ([], []) = EQUAL
   | dict_ord _ ([], _ :: _) = LESS
-  | dict_ord _ (_ :: _, []) = GREATER
-  | dict_ord elem_ord (x :: xs, y :: ys) =
-      (case elem_ord (x, y) of EQUAL => dict_ord elem_ord (xs, ys) | ord => ord);
+  | dict_ord _ (_ :: _, []) = GREATER;
 
 (*lexicographic product of lists*)
 fun list_ord elem_ord (xs, ys) =