Use prefix component of bindings for locale prefixes.
authorballarin
Wed Dec 10 17:19:25 2008 +0100 (2008-12-10)
changeset 29208b0c81b9a0133
parent 29207 a91012d9db21
child 29209 c2a750c8a37b
child 29223 e09c53289830
Use prefix component of bindings for locale prefixes.
src/Pure/General/binding.ML
src/Pure/Isar/expression.ML
     1.1 --- a/src/Pure/General/binding.ML	Wed Dec 10 17:18:12 2008 +0100
     1.2 +++ b/src/Pure/General/binding.ML	Wed Dec 10 17:19:25 2008 +0100
     1.3 @@ -59,8 +59,8 @@
     1.4  val qualify = map_base o qualify_base;
     1.5    (*FIXME should all operations on bare names move here from name_space.ML ?*)
     1.6  
     1.7 -fun add_prefix sticky prfx b = if prfx = "" then error "empty name prefix"
     1.8 -  else (map_binding o apfst) (cons (prfx, sticky)) b;
     1.9 +fun add_prefix sticky "" b = b
    1.10 +  | add_prefix sticky prfx b = (map_binding o apfst) (cons (prfx, sticky)) b;
    1.11  
    1.12  fun map_prefix f (Binding ((prefix, name), pos)) =
    1.13    f prefix (name_pos (name, pos));
     2.1 --- a/src/Pure/Isar/expression.ML	Wed Dec 10 17:18:12 2008 +0100
     2.2 +++ b/src/Pure/Isar/expression.ML	Wed Dec 10 17:19:25 2008 +0100
     2.3 @@ -175,7 +175,7 @@
     2.4      val inst = Symtab.make insts'';
     2.5    in
     2.6      (Element.inst_morphism (ProofContext.theory_of ctxt) (instT, inst) $>
     2.7 -      Morphism.binding_morphism (Binding.qualify prfx), ctxt')
     2.8 +      Morphism.binding_morphism (Binding.add_prefix false prfx), ctxt')
     2.9    end;
    2.10  
    2.11