src/Pure/General/ord_list.ML
changeset 39687 4e9b6ada3a21
parent 33037 b22e44496dc2
child 41473 3717fc42ebe9
     1.1 --- a/src/Pure/General/ord_list.ML	Fri Sep 24 15:37:36 2010 +0200
     1.2 +++ b/src/Pure/General/ord_list.ML	Fri Sep 24 15:53:13 2010 +0200
     1.3 @@ -18,7 +18,7 @@
     1.4    val subtract: ('b * 'a -> order) -> 'b T -> 'a T -> 'a T
     1.5  end;
     1.6  
     1.7 -structure OrdList: ORD_LIST =
     1.8 +structure Ord_List: ORD_LIST =
     1.9  struct
    1.10  
    1.11  type 'a T = 'a list;