tuned name bindings

--- a/src/Pure/Isar/element.ML	Thu Nov 20 14:55:25 2008 +0100
+++ b/src/Pure/Isar/element.ML	Thu Nov 20 14:55:28 2008 +0100
@@ -138,7 +138,7 @@
 
 fun params_of (Fixes fixes) = fixes |> map
     (fn (x, SOME T, _) => (Name.name_of x, T)
-      | (x, _, _) => raise TERM ("Untyped context element parameter " ^ quote (Name.name_of x), []))
+      | (x, _, _) => raise TERM ("Untyped context element parameter " ^ quote (Name.display x), []))
   | params_of _ = [];
 
 fun prems_of (Assumes asms) = maps (map fst o snd) asms
@@ -161,9 +161,9 @@
       Pretty.block [Pretty.keyword keyword, Pretty.brk 1, x] ::
         map (fn y => Pretty.block [Pretty.str "  ", Pretty.keyword sep, Pretty.brk 1, y]) ys;
 
-fun pretty_name_atts ctxt (binding, atts) sep =
+fun pretty_name_atts ctxt (b, atts) sep =
   let
-    val name = Name.output binding;
+    val name = Name.display b;
   in if name = "" andalso null atts then []
     else [Pretty.block
       (Pretty.breaks (Pretty.str name :: Attrib.pretty_attribs ctxt atts @ [Pretty.str sep]))]
@@ -394,9 +394,9 @@
   | (SOME (x', NONE), _) => (x', NoSyn)
   | (SOME (x', SOME mx'), _) => (x', mx'));
 
-fun rename_var ren (binding, mx) =
+fun rename_var ren (b, mx) =
   let
-    val x = Name.name_of binding;
+    val x = Name.name_of b;
     val (x', mx') = rename_var_name ren (x, mx);
   in (Name.binding x', mx') end;
 

--- a/src/Pure/Isar/expression.ML	Thu Nov 20 14:55:25 2008 +0100
+++ b/src/Pure/Isar/expression.ML	Thu Nov 20 14:55:28 2008 +0100
@@ -165,7 +165,7 @@
                   (* FIXME: should check for bindings being the same.
                      Instead we check for equal name and syntax. *)
                   if mx1 = mx2 then mx1
-                  else error ("Conflicting syntax for parameter" ^ quote (Name.name_of p) ^
+                  else error ("Conflicting syntax for parameter" ^ quote (Name.display p) ^
                     " in expression.")) (ps, ps')
               in (i', ps'') end) is []
           in

--- a/src/Pure/Isar/locale.ML	Thu Nov 20 14:55:25 2008 +0100
+++ b/src/Pure/Isar/locale.ML	Thu Nov 20 14:55:28 2008 +0100
@@ -136,23 +136,23 @@
 
 (* auxiliary: noting with structured name bindings *)
 
-fun global_note_prefix kind ((binding, atts), facts_atts_s) thy =
+fun global_note_prefix kind ((b, atts), facts_atts_s) thy =
   (*FIXME belongs to theory_target.ML ?*)
   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))
+      (b, (atts, facts_atts_s))
   |>> snd
   ||> Sign.restore_naming thy;
 
-fun local_note_prefix kind ((binding, atts), facts_atts_s) ctxt =
+fun local_note_prefix kind ((b, 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))
+      (b, (atts, facts_atts_s))
   |>> snd
   ||> ProofContext.restore_naming ctxt;
 
@@ -661,7 +661,7 @@
 fun params_of' elemss =
   distinct (eq_fst (op = : string * string -> bool)) (maps (snd o fst o fst) elemss);
 
-fun param_prefix locale_name params = (NameSpace.base locale_name, space_implode "_" params);
+fun param_prefix locale_name params = (NameSpace.base locale_name ^ "_locale", space_implode "_" params);
 
 
 (* CB: param_types has the following type:
@@ -954,9 +954,9 @@
         val mode' = map_mode (map (Element.map_witness (inst_wit all_params))) mode;
         val ren = map fst ps ~~ map (fn p => (p, lookup_syn p)) params;
         val [env] = unify_parms ctxt all_params [map (apfst (Element.rename ren) o apsnd SOME) ps];
-        val (locale_name, pprfx) = param_prefix name params;
+        val (lprfx, pprfx) = param_prefix name params;
         val add_prefices = pprfx <> "" ? Name.add_prefix false pprfx
-          #> Name.add_prefix false locale_name;
+          #> Name.add_prefix false lprfx;
         val elem_morphism =
           Element.rename_morphism ren $>
           Morphism.name_morphism add_prefices $>
@@ -1257,9 +1257,9 @@
       end;
 
 
-fun finish_ext_elem parms _ (Fixes fixes, _) = Fixes (map (fn (binding, _, mx) =>
-      let val x = Name.name_of binding
-      in (binding, AList.lookup (op =) parms x, mx) end) fixes)
+fun finish_ext_elem parms _ (Fixes fixes, _) = Fixes (map (fn (b, _, mx) =>
+      let val x = Name.name_of b
+      in (b, AList.lookup (op =) parms x, mx) end) fixes)
   | finish_ext_elem parms _ (Constrains _, _) = Constrains []
   | finish_ext_elem _ close (Assumes asms, propp) =
       close (Assumes (map #1 asms ~~ propp))
@@ -1640,12 +1640,12 @@
 
 (* compute and apply morphism *)
 
-fun name_morph phi_name (locale_name, pprfx) binding =
-  binding
-  |> (if not (Name.is_nothing binding) andalso pprfx <> ""
+fun name_morph phi_name (lprfx, pprfx) b =
+  b
+  |> (if not (Name.is_nothing b) andalso pprfx <> ""
         then Name.add_prefix false pprfx else I)
-  |> (if not (Name.is_nothing binding)
-        then Name.add_prefix false (locale_name ^ "_locale") else I)
+  |> (if not (Name.is_nothing b)
+        then Name.add_prefix false lprfx else I)
   |> phi_name;
 
 fun inst_morph thy phi_name param_prfx insts prems eqns export =
@@ -2455,13 +2455,13 @@
     |> pair morphs
   end;
 
-fun standard_name_morph interp_prfx binding =
-  if Name.is_nothing binding then binding
-  else Name.map_prefix (fn ((locale_name, _) :: pprfx) =>
+fun standard_name_morph interp_prfx b =
+  if Name.is_nothing b then b
+  else Name.map_prefix (fn ((lprfx, _) :: pprfx) =>
     fold (Name.add_prefix false o fst) pprfx
     #> interp_prfx <> "" ? Name.add_prefix true interp_prfx
-    #> Name.add_prefix false locale_name
-  ) binding;
+    #> Name.add_prefix false lprfx
+  ) b;
 
 in
 

--- a/src/Pure/Isar/specification.ML	Thu Nov 20 14:55:25 2008 +0100
+++ b/src/Pure/Isar/specification.ML	Thu Nov 20 14:55:28 2008 +0100
@@ -269,8 +269,8 @@
       in ((prems, stmt, []), goal_ctxt) end
   | Element.Obtains obtains =>
       let
-        val case_names = obtains |> map_index (fn (i, (binding, _)) =>
-          let val name = Name.name_of binding
+        val case_names = obtains |> map_index (fn (i, (b, _)) =>
+          let val name = Name.name_of b
           in if name = "" then string_of_int (i + 1) else name end);
         val constraints = obtains |> map (fn (_, (vars, _)) =>
           Element.Constrains