src/Pure/Isar/locale.ML
changeset 28862 53f13f763d4f
parent 28822 7ca11ecbc4fb
child 28865 194e8f3439fe
     1.1 --- a/src/Pure/Isar/locale.ML	Thu Nov 20 14:55:25 2008 +0100
     1.2 +++ b/src/Pure/Isar/locale.ML	Thu Nov 20 14:55:28 2008 +0100
     1.3 @@ -136,23 +136,23 @@
     1.4  
     1.5  (* auxiliary: noting with structured name bindings *)
     1.6  
     1.7 -fun global_note_prefix kind ((binding, atts), facts_atts_s) thy =
     1.8 +fun global_note_prefix kind ((b, atts), facts_atts_s) thy =
     1.9    (*FIXME belongs to theory_target.ML ?*)
    1.10    thy
    1.11    |> Sign.qualified_names
    1.12    |> Sign.name_decl (fn (bname, (atts, facts_atts_s)) =>
    1.13      yield_singleton (PureThy.note_thmss kind) ((Name.binding bname, atts), facts_atts_s))
    1.14 -      (binding, (atts, facts_atts_s))
    1.15 +      (b, (atts, facts_atts_s))
    1.16    |>> snd
    1.17    ||> Sign.restore_naming thy;
    1.18  
    1.19 -fun local_note_prefix kind ((binding, atts), facts_atts_s) ctxt =
    1.20 +fun local_note_prefix kind ((b, atts), facts_atts_s) ctxt =
    1.21    (*FIXME belongs to theory_target.ML ?*)
    1.22    ctxt
    1.23    |> ProofContext.qualified_names
    1.24    |> ProofContext.name_decl (fn (bname, (atts, facts_atts_s)) =>
    1.25      yield_singleton (ProofContext.note_thmss_i kind) ((Name.binding bname, atts), facts_atts_s))
    1.26 -      (binding, (atts, facts_atts_s))
    1.27 +      (b, (atts, facts_atts_s))
    1.28    |>> snd
    1.29    ||> ProofContext.restore_naming ctxt;
    1.30  
    1.31 @@ -661,7 +661,7 @@
    1.32  fun params_of' elemss =
    1.33    distinct (eq_fst (op = : string * string -> bool)) (maps (snd o fst o fst) elemss);
    1.34  
    1.35 -fun param_prefix locale_name params = (NameSpace.base locale_name, space_implode "_" params);
    1.36 +fun param_prefix locale_name params = (NameSpace.base locale_name ^ "_locale", space_implode "_" params);
    1.37  
    1.38  
    1.39  (* CB: param_types has the following type:
    1.40 @@ -954,9 +954,9 @@
    1.41          val mode' = map_mode (map (Element.map_witness (inst_wit all_params))) mode;
    1.42          val ren = map fst ps ~~ map (fn p => (p, lookup_syn p)) params;
    1.43          val [env] = unify_parms ctxt all_params [map (apfst (Element.rename ren) o apsnd SOME) ps];
    1.44 -        val (locale_name, pprfx) = param_prefix name params;
    1.45 +        val (lprfx, pprfx) = param_prefix name params;
    1.46          val add_prefices = pprfx <> "" ? Name.add_prefix false pprfx
    1.47 -          #> Name.add_prefix false locale_name;
    1.48 +          #> Name.add_prefix false lprfx;
    1.49          val elem_morphism =
    1.50            Element.rename_morphism ren $>
    1.51            Morphism.name_morphism add_prefices $>
    1.52 @@ -1257,9 +1257,9 @@
    1.53        end;
    1.54  
    1.55  
    1.56 -fun finish_ext_elem parms _ (Fixes fixes, _) = Fixes (map (fn (binding, _, mx) =>
    1.57 -      let val x = Name.name_of binding
    1.58 -      in (binding, AList.lookup (op =) parms x, mx) end) fixes)
    1.59 +fun finish_ext_elem parms _ (Fixes fixes, _) = Fixes (map (fn (b, _, mx) =>
    1.60 +      let val x = Name.name_of b
    1.61 +      in (b, AList.lookup (op =) parms x, mx) end) fixes)
    1.62    | finish_ext_elem parms _ (Constrains _, _) = Constrains []
    1.63    | finish_ext_elem _ close (Assumes asms, propp) =
    1.64        close (Assumes (map #1 asms ~~ propp))
    1.65 @@ -1640,12 +1640,12 @@
    1.66  
    1.67  (* compute and apply morphism *)
    1.68  
    1.69 -fun name_morph phi_name (locale_name, pprfx) binding =
    1.70 -  binding
    1.71 -  |> (if not (Name.is_nothing binding) andalso pprfx <> ""
    1.72 +fun name_morph phi_name (lprfx, pprfx) b =
    1.73 +  b
    1.74 +  |> (if not (Name.is_nothing b) andalso pprfx <> ""
    1.75          then Name.add_prefix false pprfx else I)
    1.76 -  |> (if not (Name.is_nothing binding)
    1.77 -        then Name.add_prefix false (locale_name ^ "_locale") else I)
    1.78 +  |> (if not (Name.is_nothing b)
    1.79 +        then Name.add_prefix false lprfx else I)
    1.80    |> phi_name;
    1.81  
    1.82  fun inst_morph thy phi_name param_prfx insts prems eqns export =
    1.83 @@ -2455,13 +2455,13 @@
    1.84      |> pair morphs
    1.85    end;
    1.86  
    1.87 -fun standard_name_morph interp_prfx binding =
    1.88 -  if Name.is_nothing binding then binding
    1.89 -  else Name.map_prefix (fn ((locale_name, _) :: pprfx) =>
    1.90 +fun standard_name_morph interp_prfx b =
    1.91 +  if Name.is_nothing b then b
    1.92 +  else Name.map_prefix (fn ((lprfx, _) :: pprfx) =>
    1.93      fold (Name.add_prefix false o fst) pprfx
    1.94      #> interp_prfx <> "" ? Name.add_prefix true interp_prfx
    1.95 -    #> Name.add_prefix false locale_name
    1.96 -  ) binding;
    1.97 +    #> Name.add_prefix false lprfx
    1.98 +  ) b;
    1.99  
   1.100  in
   1.101