src/Pure/General/ord_list.ML
changeset 33037 b22e44496dc2
parent 30572 8fbc355100f2
child 39687 4e9b6ada3a21
     1.1 --- a/src/Pure/General/ord_list.ML	Tue Oct 20 13:37:56 2009 +0200
     1.2 +++ b/src/Pure/General/ord_list.ML	Tue Oct 20 16:13:01 2009 +0200
     1.3 @@ -56,7 +56,6 @@
     1.4  
     1.5  (* lists as sets *)
     1.6  
     1.7 -nonfix subset;
     1.8  fun subset ord (list1, list2) =
     1.9    let
    1.10      fun sub [] _ = true
    1.11 @@ -75,7 +74,6 @@
    1.12  fun handle_same f x = f x handle SAME => x;
    1.13  
    1.14  (*union: insert elements of first list into second list*)
    1.15 -nonfix union;
    1.16  fun union ord list1 list2 =
    1.17    let
    1.18      fun unio [] _ = raise SAME
    1.19 @@ -88,7 +86,6 @@
    1.20    in if pointer_eq (list1, list2) then list1 else handle_same (unio list1) list2 end;
    1.21  
    1.22  (*intersection: filter second list for elements present in first list*)
    1.23 -nonfix inter;
    1.24  fun inter ord list1 list2 =
    1.25    let
    1.26      fun intr _ [] = raise SAME