added qualified: string -> binding -> binding;
authorwenzelm
Wed, 03 Sep 2008 11:44:52 +0200
changeset 28108 1b08ed83b79e
parent 28107 760ecc6fc1bd
child 28109 3f76ae637f71
added qualified: string -> binding -> binding;
src/Pure/name.ML
--- 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;