# HG changeset patch
# User wenzelm
# Date 1220435092 -7200
# Node ID 1b08ed83b79e185f5c5895a0aaa312815705cc6f
# Parent  760ecc6fc1bd93cb7ba9065222a0dd3649761b21
added qualified: string -> binding -> binding;

diff -r 760ecc6fc1bd -r 1b08ed83b79e 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;