# HG changeset patch
# User ballarin
# Date 1228925965 -3600
# Node ID b0c81b9a013359b9b76df6a4c62531262abf0cf4
# Parent  a91012d9db21f03fc022cdc574acc316a2d9514a
Use prefix component of bindings for locale prefixes.

diff -r a91012d9db21 -r b0c81b9a0133 src/Pure/General/binding.ML
--- 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));
diff -r a91012d9db21 -r b0c81b9a0133 src/Pure/Isar/expression.ML
--- 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;