added qualified: string -> binding -> binding;
authorwenzelm
Wed Sep 03 11:44:52 2008 +0200 (2008-09-03)
changeset 281081b08ed83b79e
parent 28107 760ecc6fc1bd
child 28109 3f76ae637f71
added qualified: string -> binding -> binding;
src/Pure/name.ML
     1.1 --- a/src/Pure/name.ML	Wed Sep 03 11:44:48 2008 +0200
     1.2 +++ b/src/Pure/name.ML	Wed Sep 03 11:44:52 2008 +0200
     1.3 @@ -35,6 +35,7 @@
     1.4    val name_of: binding -> string
     1.5    val pos_of: binding -> Position.T
     1.6    val map_name: (string -> string) -> binding -> binding
     1.7 +  val qualified: string -> binding -> binding
     1.8  end;
     1.9  
    1.10  structure Name: NAME =
    1.11 @@ -160,5 +161,6 @@
    1.12  fun pos_of (Binding (_, pos)) = pos;
    1.13  
    1.14  fun map_name f (Binding (name, pos)) = Binding (f name, pos);
    1.15 +val qualified = map_name o NameSpace.qualified;
    1.16  
    1.17  end;