1.1 --- a/src/Pure/Isar/element.ML	Thu Nov 20 14:55:25 2008 +0100
     1.2 +++ b/src/Pure/Isar/element.ML	Thu Nov 20 14:55:28 2008 +0100
     1.3 @@ -138,7 +138,7 @@
     1.4  
     1.5  fun params_of (Fixes fixes) = fixes |> map
     1.6      (fn (x, SOME T, _) => (Name.name_of x, T)
     1.7 -      | (x, _, _) => raise TERM ("Untyped context element parameter " ^ quote (Name.name_of x), []))
     1.8 +      | (x, _, _) => raise TERM ("Untyped context element parameter " ^ quote (Name.display x), []))
     1.9    | params_of _ = [];
    1.10  
    1.11  fun prems_of (Assumes asms) = maps (map fst o snd) asms
    1.12 @@ -161,9 +161,9 @@
    1.13        Pretty.block [Pretty.keyword keyword, Pretty.brk 1, x] ::
    1.14          map (fn y => Pretty.block [Pretty.str "  ", Pretty.keyword sep, Pretty.brk 1, y]) ys;
    1.15  
    1.16 -fun pretty_name_atts ctxt (binding, atts) sep =
    1.17 +fun pretty_name_atts ctxt (b, atts) sep =
    1.18    let
    1.19 -    val name = Name.output binding;
    1.20 +    val name = Name.display b;
    1.21    in if name = "" andalso null atts then []
    1.22      else [Pretty.block
    1.23        (Pretty.breaks (Pretty.str name :: Attrib.pretty_attribs ctxt atts @ [Pretty.str sep]))]
    1.24 @@ -394,9 +394,9 @@
    1.25    | (SOME (x', NONE), _) => (x', NoSyn)
    1.26    | (SOME (x', SOME mx'), _) => (x', mx'));
    1.27  
    1.28 -fun rename_var ren (binding, mx) =
    1.29 +fun rename_var ren (b, mx) =
    1.30    let
    1.31 -    val x = Name.name_of binding;
    1.32 +    val x = Name.name_of b;
    1.33      val (x', mx') = rename_var_name ren (x, mx);
    1.34    in (Name.binding x', mx') end;
    1.35  

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

     3.1 --- a/src/Pure/Isar/locale.ML	Thu Nov 20 14:55:25 2008 +0100
     3.2 +++ b/src/Pure/Isar/locale.ML	Thu Nov 20 14:55:28 2008 +0100
     3.3 @@ -136,23 +136,23 @@
     3.4  
     3.5  (* auxiliary: noting with structured name bindings *)
     3.6  
     3.7 -fun global_note_prefix kind ((binding, atts), facts_atts_s) thy =
     3.8 +fun global_note_prefix kind ((b, atts), facts_atts_s) thy =
     3.9    (*FIXME belongs to theory_target.ML ?*)
    3.10    thy
    3.11    |> Sign.qualified_names
    3.12    |> Sign.name_decl (fn (bname, (atts, facts_atts_s)) =>
    3.13      yield_singleton (PureThy.note_thmss kind) ((Name.binding bname, atts), facts_atts_s))
    3.14 -      (binding, (atts, facts_atts_s))
    3.15 +      (b, (atts, facts_atts_s))
    3.16    |>> snd
    3.17    ||> Sign.restore_naming thy;
    3.18  
    3.19 -fun local_note_prefix kind ((binding, atts), facts_atts_s) ctxt =
    3.20 +fun local_note_prefix kind ((b, atts), facts_atts_s) ctxt =
    3.21    (*FIXME belongs to theory_target.ML ?*)
    3.22    ctxt
    3.23    |> ProofContext.qualified_names
    3.24    |> ProofContext.name_decl (fn (bname, (atts, facts_atts_s)) =>
    3.25      yield_singleton (ProofContext.note_thmss_i kind) ((Name.binding bname, atts), facts_atts_s))
    3.26 -      (binding, (atts, facts_atts_s))
    3.27 +      (b, (atts, facts_atts_s))
    3.28    |>> snd
    3.29    ||> ProofContext.restore_naming ctxt;
    3.30  
    3.31 @@ -661,7 +661,7 @@
    3.32  fun params_of' elemss =
    3.33    distinct (eq_fst (op = : string * string -> bool)) (maps (snd o fst o fst) elemss);
    3.34  
    3.35 -fun param_prefix locale_name params = (NameSpace.base locale_name, space_implode "_" params);
    3.36 +fun param_prefix locale_name params = (NameSpace.base locale_name ^ "_locale", space_implode "_" params);
    3.37  
    3.38  
    3.39  (* CB: param_types has the following type:
    3.40 @@ -954,9 +954,9 @@
    3.41          val mode' = map_mode (map (Element.map_witness (inst_wit all_params))) mode;
    3.42          val ren = map fst ps ~~ map (fn p => (p, lookup_syn p)) params;
    3.43          val [env] = unify_parms ctxt all_params [map (apfst (Element.rename ren) o apsnd SOME) ps];
    3.44 -        val (locale_name, pprfx) = param_prefix name params;
    3.45 +        val (lprfx, pprfx) = param_prefix name params;
    3.46          val add_prefices = pprfx <> "" ? Name.add_prefix false pprfx
    3.47 -          #> Name.add_prefix false locale_name;
    3.48 +          #> Name.add_prefix false lprfx;
    3.49          val elem_morphism =
    3.50            Element.rename_morphism ren $>
    3.51            Morphism.name_morphism add_prefices $>
    3.52 @@ -1257,9 +1257,9 @@
    3.53        end;
    3.54  
    3.55  
    3.56 -fun finish_ext_elem parms _ (Fixes fixes, _) = Fixes (map (fn (binding, _, mx) =>
    3.57 -      let val x = Name.name_of binding
    3.58 -      in (binding, AList.lookup (op =) parms x, mx) end) fixes)
    3.59 +fun finish_ext_elem parms _ (Fixes fixes, _) = Fixes (map (fn (b, _, mx) =>
    3.60 +      let val x = Name.name_of b
    3.61 +      in (b, AList.lookup (op =) parms x, mx) end) fixes)
    3.62    | finish_ext_elem parms _ (Constrains _, _) = Constrains []
    3.63    | finish_ext_elem _ close (Assumes asms, propp) =
    3.64        close (Assumes (map #1 asms ~~ propp))
    3.65 @@ -1640,12 +1640,12 @@
    3.66  
    3.67  (* compute and apply morphism *)
    3.68  
    3.69 -fun name_morph phi_name (locale_name, pprfx) binding =
    3.70 -  binding
    3.71 -  |> (if not (Name.is_nothing binding) andalso pprfx <> ""
    3.72 +fun name_morph phi_name (lprfx, pprfx) b =
    3.73 +  b
    3.74 +  |> (if not (Name.is_nothing b) andalso pprfx <> ""
    3.75          then Name.add_prefix false pprfx else I)
    3.76 -  |> (if not (Name.is_nothing binding)
    3.77 -        then Name.add_prefix false (locale_name ^ "_locale") else I)
    3.78 +  |> (if not (Name.is_nothing b)
    3.79 +        then Name.add_prefix false lprfx else I)
    3.80    |> phi_name;
    3.81  
    3.82  fun inst_morph thy phi_name param_prfx insts prems eqns export =
    3.83 @@ -2455,13 +2455,13 @@
    3.84      |> pair morphs
    3.85    end;
    3.86  
    3.87 -fun standard_name_morph interp_prfx binding =
    3.88 -  if Name.is_nothing binding then binding
    3.89 -  else Name.map_prefix (fn ((locale_name, _) :: pprfx) =>
    3.90 +fun standard_name_morph interp_prfx b =
    3.91 +  if Name.is_nothing b then b
    3.92 +  else Name.map_prefix (fn ((lprfx, _) :: pprfx) =>
    3.93      fold (Name.add_prefix false o fst) pprfx
    3.94      #> interp_prfx <> "" ? Name.add_prefix true interp_prfx
    3.95 -    #> Name.add_prefix false locale_name
    3.96 -  ) binding;
    3.97 +    #> Name.add_prefix false lprfx
    3.98 +  ) b;
    3.99  
   3.100  in
   3.101  

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