author | wenzelm |
Wed, 03 Sep 2008 11:44:52 +0200 | |
changeset 28108 | 1b08ed83b79e |
parent 28107 | 760ecc6fc1bd |
child 28109 | 3f76ae637f71 |
src/Pure/name.ML | file | annotate | diff | comparison | revisions |
--- a/src/Pure/name.ML Wed Sep 03 11:44:48 2008 +0200 +++ b/src/Pure/name.ML Wed Sep 03 11:44:52 2008 +0200 @@ -35,6 +35,7 @@ val name_of: binding -> string val pos_of: binding -> Position.T val map_name: (string -> string) -> binding -> binding + val qualified: string -> binding -> binding end; structure Name: NAME = @@ -160,5 +161,6 @@ fun pos_of (Binding (_, pos)) = pos; fun map_name f (Binding (name, pos)) = Binding (f name, pos); +val qualified = map_name o NameSpace.qualified; end;