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