src/Pure/Isar/locale.ML
changeset 28865 194e8f3439fe
parent 28862 53f13f763d4f
child 28893 4e6fd31c9883
     1.1 --- a/src/Pure/Isar/locale.ML	Thu Nov 20 19:06:03 2008 +0100
     1.2 +++ b/src/Pure/Isar/locale.ML	Thu Nov 20 19:06:05 2008 +0100
     1.3 @@ -91,7 +91,7 @@
     1.4    val intro_locales_tac: bool -> Proof.context -> thm list -> tactic
     1.5  
     1.6    (* Storing results *)
     1.7 -  val local_note_prefix: string ->
     1.8 +  val local_note_qualified: string ->
     1.9      (Name.binding * attribute list) * (thm list * attribute list) list ->
    1.10      Proof.context -> (string * thm list) * Proof.context
    1.11    val add_thmss: string -> string -> (Attrib.binding * (thm list * Attrib.src list) list) list ->
    1.12 @@ -136,24 +136,16 @@
    1.13  
    1.14  (* auxiliary: noting with structured name bindings *)
    1.15  
    1.16 -fun global_note_prefix kind ((b, atts), facts_atts_s) thy =
    1.17 -  (*FIXME belongs to theory_target.ML ?*)
    1.18 +fun global_note_qualified kind ((b, atts), facts_atts_s) thy =
    1.19    thy
    1.20    |> Sign.qualified_names
    1.21 -  |> Sign.name_decl (fn (bname, (atts, facts_atts_s)) =>
    1.22 -    yield_singleton (PureThy.note_thmss kind) ((Name.binding bname, atts), facts_atts_s))
    1.23 -      (b, (atts, facts_atts_s))
    1.24 -  |>> snd
    1.25 +  |> yield_singleton (PureThy.note_thmss kind) ((b, atts), facts_atts_s)
    1.26    ||> Sign.restore_naming thy;
    1.27  
    1.28 -fun local_note_prefix kind ((b, atts), facts_atts_s) ctxt =
    1.29 -  (*FIXME belongs to theory_target.ML ?*)
    1.30 +fun local_note_qualified kind ((b, atts), facts_atts_s) ctxt =
    1.31    ctxt
    1.32    |> ProofContext.qualified_names
    1.33 -  |> ProofContext.name_decl (fn (bname, (atts, facts_atts_s)) =>
    1.34 -    yield_singleton (ProofContext.note_thmss_i kind) ((Name.binding bname, atts), facts_atts_s))
    1.35 -      (b, (atts, facts_atts_s))
    1.36 -  |>> snd
    1.37 +  |> yield_singleton (ProofContext.note_thmss_i kind) ((b, atts), facts_atts_s)
    1.38    ||> ProofContext.restore_naming ctxt;
    1.39  
    1.40  
    1.41 @@ -1018,7 +1010,7 @@
    1.42    | activate_elem _ is_ext (Notes (kind, facts)) (ctxt, mode) =
    1.43        let
    1.44          val facts' = Attrib.map_facts (Attrib.attribute_i (ProofContext.theory_of ctxt)) facts;
    1.45 -        val (res, ctxt') = ctxt |> fold_map (local_note_prefix kind) facts';
    1.46 +        val (res, ctxt') = ctxt |> fold_map (local_note_qualified kind) facts';
    1.47        in (if is_ext then (map (#1 o #1) facts' ~~ map #2 res) else [], (ctxt', mode)) end;
    1.48  
    1.49  fun activate_elems ax_in_ctxt (((name, ps), mode), elems) ctxt =
    1.50 @@ -1704,7 +1696,7 @@
    1.51                 (Attrib.attribute_i thy) insts prems eqns exp;
    1.52        in
    1.53          thy
    1.54 -        |> fold (snd oo global_note_prefix kind) args'
    1.55 +        |> fold (snd oo global_note_qualified kind) args'
    1.56        end;
    1.57    in fold activate regs thy end;
    1.58  
    1.59 @@ -2154,7 +2146,7 @@
    1.60  
    1.61  fun global_activate_facts_elemss x = gen_activate_facts_elemss
    1.62    ProofContext.init
    1.63 -  global_note_prefix
    1.64 +  global_note_qualified
    1.65    Attrib.attribute_i
    1.66    put_global_registration
    1.67    add_global_witness
    1.68 @@ -2163,7 +2155,7 @@
    1.69  
    1.70  fun local_activate_facts_elemss x = gen_activate_facts_elemss
    1.71    I
    1.72 -  local_note_prefix
    1.73 +  local_note_qualified
    1.74    (Attrib.attribute_i o ProofContext.theory_of)
    1.75    put_local_registration
    1.76    add_local_witness
    1.77 @@ -2400,7 +2392,7 @@
    1.78                      |> (map o apfst o apfst) (name_morph phi_name param_prfx);
    1.79                  in
    1.80                    thy
    1.81 -                  |> fold (snd oo global_note_prefix kind) facts'
    1.82 +                  |> fold (snd oo global_note_qualified kind) facts'
    1.83                  end
    1.84                | activate_elem _ _ thy = thy;
    1.85