src/Pure/library.ML
changeset 16984 abc48b981e60
parent 16878 07213f0e291f
child 17028 a497f621bfd4
     1.1 --- a/src/Pure/library.ML	Mon Aug 01 19:20:37 2005 +0200
     1.2 +++ b/src/Pure/library.ML	Mon Aug 01 19:20:38 2005 +0200
     1.3 @@ -1144,11 +1144,11 @@
     1.4    (case a_ord (x, x') of EQUAL => b_ord (y, y') | ord => ord);
     1.5  
     1.6  (*dictionary order -- in general NOT well-founded!*)
     1.7 -fun dict_ord _ ([], []) = EQUAL
     1.8 +fun dict_ord elem_ord (x :: xs, y :: ys) =
     1.9 +      (case elem_ord (x, y) of EQUAL => dict_ord elem_ord (xs, ys) | ord => ord)
    1.10 +  | dict_ord _ ([], []) = EQUAL
    1.11    | dict_ord _ ([], _ :: _) = LESS
    1.12 -  | dict_ord _ (_ :: _, []) = GREATER
    1.13 -  | dict_ord elem_ord (x :: xs, y :: ys) =
    1.14 -      (case elem_ord (x, y) of EQUAL => dict_ord elem_ord (xs, ys) | ord => ord);
    1.15 +  | dict_ord _ (_ :: _, []) = GREATER;
    1.16  
    1.17  (*lexicographic product of lists*)
    1.18  fun list_ord elem_ord (xs, ys) =