Use prefix component of bindings for locale prefixes.

--- a/src/Pure/General/binding.ML	Wed Dec 10 17:18:12 2008 +0100
+++ b/src/Pure/General/binding.ML	Wed Dec 10 17:19:25 2008 +0100
@@ -59,8 +59,8 @@
 val qualify = map_base o qualify_base;
   (*FIXME should all operations on bare names move here from name_space.ML ?*)
 
-fun add_prefix sticky prfx b = if prfx = "" then error "empty name prefix"
-  else (map_binding o apfst) (cons (prfx, sticky)) b;
+fun add_prefix sticky "" b = b
+  | add_prefix sticky prfx b = (map_binding o apfst) (cons (prfx, sticky)) b;
 
 fun map_prefix f (Binding ((prefix, name), pos)) =
   f prefix (name_pos (name, pos));

--- a/src/Pure/Isar/expression.ML	Wed Dec 10 17:18:12 2008 +0100
+++ b/src/Pure/Isar/expression.ML	Wed Dec 10 17:19:25 2008 +0100
@@ -175,7 +175,7 @@
     val inst = Symtab.make insts'';
   in
     (Element.inst_morphism (ProofContext.theory_of ctxt) (instT, inst) $>
-      Morphism.binding_morphism (Binding.qualify prfx), ctxt')
+      Morphism.binding_morphism (Binding.add_prefix false prfx), ctxt')
   end;