namify and name_decl combinators

--- a/src/Pure/Isar/locale.ML	Fri Nov 14 08:50:09 2008 +0100
+++ b/src/Pure/Isar/locale.ML	Fri Nov 14 08:50:10 2008 +0100
@@ -139,33 +139,25 @@
 
 (* auxiliary: noting with structured name bindings *)
 
-fun global_note_prefix kind ((bnd, atts), facts_atts_s) thy =
-  (*FIXME belongs to theory_target.ML*)
-  let
-    val prfx = Name.prefix_of bnd;
-    val name = Name.name_of bnd;
-  in
-    thy
-    |> Sign.qualified_names
-    |> fold (fn (prfx_seg, sticky) =>
-        (if sticky then Sign.sticky_prefix else Sign.add_path) prfx_seg) prfx
-    |> yield_singleton (PureThy.note_thmss kind) ((Name.binding name, atts), facts_atts_s)
-    ||> Sign.restore_naming thy
-  end;
-
-fun local_note_prefix kind ((bnd, atts), facts_atts_s) ctxt =
+fun global_note_prefix kind ((binding, atts), facts_atts_s) thy =
   (*FIXME belongs to theory_target.ML ?*)
-  let
-    val prfx = Name.prefix_of bnd;
-    val name = Name.name_of bnd;
-  in
-    ctxt
-    |> ProofContext.qualified_names
-    |> fold (fn (prfx_seg, sticky) =>
-        (if sticky then ProofContext.sticky_prefix else ProofContext.add_path) prfx_seg) prfx
-    |> yield_singleton (ProofContext.note_thmss_i kind) ((Name.binding name, atts), facts_atts_s)
-    ||> ProofContext.restore_naming ctxt
-  end;
+  thy
+  |> Sign.qualified_names
+  |> Sign.name_decl (fn (bname, (atts, facts_atts_s)) =>
+    yield_singleton (PureThy.note_thmss kind) ((Name.binding bname, atts), facts_atts_s))
+      (binding, (atts, facts_atts_s))
+  |>> snd
+  ||> Sign.restore_naming thy;
+
+fun local_note_prefix kind ((binding, atts), facts_atts_s) ctxt =
+  (*FIXME belongs to theory_target.ML ?*)
+  ctxt
+  |> ProofContext.qualified_names
+  |> ProofContext.name_decl (fn (bname, (atts, facts_atts_s)) =>
+    yield_singleton (ProofContext.note_thmss_i kind) ((Name.binding bname, atts), facts_atts_s))
+      (binding, (atts, facts_atts_s))
+  |>> snd
+  ||> ProofContext.restore_naming ctxt;
 
 
 (** locale elements and expressions **)
@@ -1657,9 +1649,9 @@
 
 (* compute and apply morphism *)
 
-fun add_prefixes loc (sticky, interp_prfx) param_prfx bnd =
-  bnd
-  |> (if sticky andalso Name.name_of bnd <> "" andalso param_prfx <> ""
+fun add_prefixes loc (sticky, interp_prfx) param_prfx binding =
+  binding
+  |> (if sticky andalso not (Name.is_nothing binding) andalso param_prfx <> ""
         then Name.add_prefix false param_prfx else I)
   |> Name.add_prefix sticky interp_prfx
   |> Name.add_prefix false (NameSpace.base loc ^ "_locale");
@@ -1684,7 +1676,7 @@
 fun activate_note thy loc (sticky, interp_prfx) param_prfx attrib insts prems eqns exp =
   (Element.facts_map o Element.morph_ctxt)
       (inst_morph thy loc (sticky, interp_prfx) param_prfx insts prems eqns exp)
-  #> Attrib.map_facts attrib (*o Args.morph_values (Morphism.name_morphism (add_prefixes loc (sticky, interp_prfx) param_prfx))*);
+  #> Attrib.map_facts attrib;
 
 
 (* public interface to interpretation morphism *)

--- a/src/Pure/Isar/proof_context.ML	Fri Nov 14 08:50:09 2008 +0100
+++ b/src/Pure/Isar/proof_context.ML	Fri Nov 14 08:50:10 2008 +0100
@@ -23,6 +23,8 @@
   val abbrev_mode: Proof.context -> bool
   val set_stmt: bool -> Proof.context -> Proof.context
   val naming_of: Proof.context -> NameSpace.naming
+  val name_decl: (string * 'a -> Proof.context -> 'b * Proof.context)
+    -> Name.binding * 'a -> Proof.context -> (string * 'b) * Proof.context
   val full_name: Proof.context -> bstring -> string
   val consts_of: Proof.context -> Consts.T
   val const_syntax_name: Proof.context -> string -> string
@@ -245,6 +247,19 @@
   map_mode (fn (_, pattern, schematic, abbrev) => (stmt, pattern, schematic, abbrev));
 
 val naming_of = #naming o rep_context;
+
+fun name_decl decl (binding, x) ctxt =
+  let
+    val naming = naming_of ctxt;
+    val (naming', name) = Name.namify naming binding;
+  in
+    ctxt
+    |> map_naming (K naming')
+    |> decl (Name.name_of binding, x)
+    |>> pair name
+    ||> map_naming (K naming)
+  end;
+
 val full_name = NameSpace.full o naming_of;
 
 val syntax_of = #syntax o rep_context;

--- a/src/Pure/name.ML	Fri Nov 14 08:50:09 2008 +0100
+++ b/src/Pure/name.ML	Fri Nov 14 08:50:10 2008 +0100
@@ -34,10 +34,12 @@
   val no_binding: binding
   val prefix_of: binding -> (string * bool) list
   val name_of: binding -> string
+  val is_nothing: binding -> bool
   val pos_of: binding -> Position.T
   val add_prefix: bool -> string -> binding -> binding
   val map_name: (string -> string) -> binding -> binding
   val qualified: string -> binding -> binding
+  val namify: NameSpace.naming -> binding -> NameSpace.naming * string
   val output: binding -> string
 end;
 
@@ -172,6 +174,15 @@
 val map_name = map_binding o apfst o apsnd;
 val qualified = map_name o NameSpace.qualified;
 
+fun is_nothing (Binding ((_, name), _)) = name = "";
+
+fun namify naming (Binding ((prefix, name), _)) =
+  let
+    fun mk_prefix (prfx, true) = NameSpace.sticky_prefix prfx
+      | mk_prefix (prfx, false) = NameSpace.add_path prfx;
+    val naming' = fold mk_prefix prefix naming;
+  in (naming', NameSpace.full naming' name) end;
+
 fun output (Binding ((prefix, name), _)) =
   if null prefix orelse name = "" then name
   else NameSpace.implode (map fst prefix) ^ " / " ^ name;

--- a/src/Pure/sign.ML	Fri Nov 14 08:50:09 2008 +0100
+++ b/src/Pure/sign.ML	Fri Nov 14 08:50:10 2008 +0100
@@ -15,6 +15,8 @@
     consts: Consts.T}
   val naming_of: theory -> NameSpace.naming
   val base_name: string -> bstring
+  val name_decl: (string * 'a -> theory -> 'b * theory)
+    -> Name.binding * 'a -> theory -> (string * 'b) * theory
   val full_name: theory -> bstring -> string
   val full_name_path: theory -> string -> bstring -> string
   val declare_name: theory -> string -> NameSpace.T -> NameSpace.T
@@ -187,6 +189,20 @@
 
 val naming_of = #naming o rep_sg;
 val base_name = NameSpace.base;
+
+fun name_decl decl (binding, x) thy =
+  let
+    val naming = naming_of thy;
+    val (naming', name) = Name.namify naming binding;
+  in
+    thy
+    |> map_naming (K naming')
+    |> decl (Name.name_of binding, x)
+    |>> pair name
+    ||> map_naming (K naming)
+  end;
+
+val namify = Name.namify o naming_of;
 val full_name = NameSpace.full o naming_of;
 fun full_name_path thy elems = NameSpace.full (NameSpace.add_path elems (naming_of thy));
 val declare_name = NameSpace.declare o naming_of;

--- a/src/Pure/simplifier.ML	Fri Nov 14 08:50:09 2008 +0100
+++ b/src/Pure/simplifier.ML	Fri Nov 14 08:50:10 2008 +0100
@@ -194,13 +194,11 @@
   in
     lthy |> LocalTheory.declaration (fn phi =>
       let
-        val binding = Morphism.name phi (Name.binding name);
-        val name' = NameSpace.implode
-          (map fst (Name.prefix_of binding) @ [Name.name_of binding]);
+        val (naming', name) = Name.namify naming (Morphism.name phi (Name.binding name));
         val simproc' = morph_simproc phi simproc;
       in
         Simprocs.map (fn simprocs =>
-            NameSpace.extend_table naming [(name', simproc')] simprocs
+            NameSpace.extend_table naming' [(name, simproc')] simprocs
               handle Symtab.DUP dup => err_dup_simproc dup)
         #> map_ss (fn ss => ss addsimprocs [simproc'])
       end)