changeset 16534 | 95460b6eb712 |
parent 16511 | dad516b121cd |
child 16680 | 346120708998 |
--- a/src/Pure/General/ord_list.ML Wed Jun 22 19:41:18 2005 +0200 +++ b/src/Pure/General/ord_list.ML Wed Jun 22 19:41:19 2005 +0200 @@ -66,7 +66,7 @@ | GREATER => sub lst1 ys); in sub list1 list2 end; -fun eq_set ord lists = list_ord ord lists = EQUAL; +fun eq_set ord lists = (list_ord ord lists = EQUAL); (* algebraic operations *)