Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/Pure/library.ML
changeset 16984 abc48b981e60
parent 16878 07213f0e291f
child 17028 a497f621bfd4 
--- 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) =
isabelle