src/Pure/General/name_space.ML
changeset 15531 08c8dad8e399
parent 15016 bcbef8418da5
child 15570 8d8c70b41bab
     1.1 --- a/src/Pure/General/name_space.ML	Fri Feb 11 18:51:00 2005 +0100
     1.2 +++ b/src/Pure/General/name_space.ML	Sun Feb 13 17:15:14 2005 +0100
     1.3 @@ -133,11 +133,11 @@
     1.4  
     1.5  fun lookup (NameSpace tab) xname =
     1.6    (case Symtab.lookup (tab, xname) of
     1.7 -    None => (xname, true)
     1.8 -  | Some ([name], _) => (name, true)
     1.9 -  | Some (name :: _, _) => (name, false)
    1.10 -  | Some ([], []) => (xname, true)
    1.11 -  | Some ([], name' :: _) => (hidden name', true));
    1.12 +    NONE => (xname, true)
    1.13 +  | SOME ([name], _) => (name, true)
    1.14 +  | SOME (name :: _, _) => (name, false)
    1.15 +  | SOME ([], []) => (xname, true)
    1.16 +  | SOME ([], name' :: _) => (hidden name', true));
    1.17  
    1.18  fun intern spc xname = #1 (lookup spc xname);
    1.19  
    1.20 @@ -170,8 +170,8 @@
    1.21  
    1.22  (* dest *)
    1.23  
    1.24 -fun dest_entry (xname, ([], _)) = None
    1.25 -  | dest_entry (xname, (name :: _, _)) = Some (name, xname);
    1.26 +fun dest_entry (xname, ([], _)) = NONE
    1.27 +  | dest_entry (xname, (name :: _, _)) = SOME (name, xname);
    1.28  
    1.29  fun dest (NameSpace tab) =
    1.30    map (apsnd (sort (int_ord o pairself size)))