src/Pure/Isar/locale.ML
changeset 28792 1d80cee865de
parent 28739 bbb5f83ce602
child 28794 4493633ab401
     1.1 --- a/src/Pure/Isar/locale.ML	Fri Nov 14 08:50:09 2008 +0100
     1.2 +++ b/src/Pure/Isar/locale.ML	Fri Nov 14 08:50:10 2008 +0100
     1.3 @@ -139,33 +139,25 @@
     1.4  
     1.5  (* auxiliary: noting with structured name bindings *)
     1.6  
     1.7 -fun global_note_prefix kind ((bnd, atts), facts_atts_s) thy =
     1.8 -  (*FIXME belongs to theory_target.ML*)
     1.9 -  let
    1.10 -    val prfx = Name.prefix_of bnd;
    1.11 -    val name = Name.name_of bnd;
    1.12 -  in
    1.13 -    thy
    1.14 -    |> Sign.qualified_names
    1.15 -    |> fold (fn (prfx_seg, sticky) =>
    1.16 -        (if sticky then Sign.sticky_prefix else Sign.add_path) prfx_seg) prfx
    1.17 -    |> yield_singleton (PureThy.note_thmss kind) ((Name.binding name, atts), facts_atts_s)
    1.18 -    ||> Sign.restore_naming thy
    1.19 -  end;
    1.20 -
    1.21 -fun local_note_prefix kind ((bnd, atts), facts_atts_s) ctxt =
    1.22 +fun global_note_prefix kind ((binding, atts), facts_atts_s) thy =
    1.23    (*FIXME belongs to theory_target.ML ?*)
    1.24 -  let
    1.25 -    val prfx = Name.prefix_of bnd;
    1.26 -    val name = Name.name_of bnd;
    1.27 -  in
    1.28 -    ctxt
    1.29 -    |> ProofContext.qualified_names
    1.30 -    |> fold (fn (prfx_seg, sticky) =>
    1.31 -        (if sticky then ProofContext.sticky_prefix else ProofContext.add_path) prfx_seg) prfx
    1.32 -    |> yield_singleton (ProofContext.note_thmss_i kind) ((Name.binding name, atts), facts_atts_s)
    1.33 -    ||> ProofContext.restore_naming ctxt
    1.34 -  end;
    1.35 +  thy
    1.36 +  |> Sign.qualified_names
    1.37 +  |> Sign.name_decl (fn (bname, (atts, facts_atts_s)) =>
    1.38 +    yield_singleton (PureThy.note_thmss kind) ((Name.binding bname, atts), facts_atts_s))
    1.39 +      (binding, (atts, facts_atts_s))
    1.40 +  |>> snd
    1.41 +  ||> Sign.restore_naming thy;
    1.42 +
    1.43 +fun local_note_prefix kind ((binding, atts), facts_atts_s) ctxt =
    1.44 +  (*FIXME belongs to theory_target.ML ?*)
    1.45 +  ctxt
    1.46 +  |> ProofContext.qualified_names
    1.47 +  |> ProofContext.name_decl (fn (bname, (atts, facts_atts_s)) =>
    1.48 +    yield_singleton (ProofContext.note_thmss_i kind) ((Name.binding bname, atts), facts_atts_s))
    1.49 +      (binding, (atts, facts_atts_s))
    1.50 +  |>> snd
    1.51 +  ||> ProofContext.restore_naming ctxt;
    1.52  
    1.53  
    1.54  (** locale elements and expressions **)
    1.55 @@ -1657,9 +1649,9 @@
    1.56  
    1.57  (* compute and apply morphism *)
    1.58  
    1.59 -fun add_prefixes loc (sticky, interp_prfx) param_prfx bnd =
    1.60 -  bnd
    1.61 -  |> (if sticky andalso Name.name_of bnd <> "" andalso param_prfx <> ""
    1.62 +fun add_prefixes loc (sticky, interp_prfx) param_prfx binding =
    1.63 +  binding
    1.64 +  |> (if sticky andalso not (Name.is_nothing binding) andalso param_prfx <> ""
    1.65          then Name.add_prefix false param_prfx else I)
    1.66    |> Name.add_prefix sticky interp_prfx
    1.67    |> Name.add_prefix false (NameSpace.base loc ^ "_locale");
    1.68 @@ -1684,7 +1676,7 @@
    1.69  fun activate_note thy loc (sticky, interp_prfx) param_prfx attrib insts prems eqns exp =
    1.70    (Element.facts_map o Element.morph_ctxt)
    1.71        (inst_morph thy loc (sticky, interp_prfx) param_prfx insts prems eqns exp)
    1.72 -  #> Attrib.map_facts attrib (*o Args.morph_values (Morphism.name_morphism (add_prefixes loc (sticky, interp_prfx) param_prfx))*);
    1.73 +  #> Attrib.map_facts attrib;
    1.74  
    1.75  
    1.76  (* public interface to interpretation morphism *)