src/Pure/Isar/locale.ML
changeset 28940 df0cb410be35
parent 28927 7e631979922f
child 28941 128459bd72d2
     1.1 --- a/src/Pure/Isar/locale.ML	Mon Dec 01 14:56:08 2008 +0100
     1.2 +++ b/src/Pure/Isar/locale.ML	Mon Dec 01 16:02:57 2008 +0100
     1.3 @@ -92,8 +92,8 @@
     1.4  
     1.5    (* Storing results *)
     1.6    val local_note_qualified: string ->
     1.7 -    (Name.binding * attribute list) * (thm list * attribute list) list ->
     1.8 -    Proof.context -> (string * thm list) * Proof.context
     1.9 +    ((Name.binding * attribute list) * (thm list * attribute list) list) list ->
    1.10 +    Proof.context -> (string * thm list) list * Proof.context
    1.11    val add_thmss: string -> string -> (Attrib.binding * (thm list * Attrib.src list) list) list ->
    1.12      Proof.context -> Proof.context
    1.13    val add_type_syntax: string -> declaration -> Proof.context -> Proof.context
    1.14 @@ -134,18 +134,18 @@
    1.15  fun merge_alists eq xs = merge_lists (eq_fst eq) xs;
    1.16  
    1.17  
    1.18 -(* auxiliary: noting with structured name bindings *)
    1.19 -
    1.20 -fun global_note_qualified kind ((b, atts), facts_atts_s) thy =
    1.21 +(* auxiliary: noting name bindings with qualified base names *)
    1.22 +
    1.23 +fun global_note_qualified kind facts thy =
    1.24    thy
    1.25    |> Sign.qualified_names
    1.26 -  |> yield_singleton (PureThy.note_thmss kind) ((b, atts), facts_atts_s)
    1.27 +  |> PureThy.note_thmss kind facts
    1.28    ||> Sign.restore_naming thy;
    1.29  
    1.30 -fun local_note_qualified kind ((b, atts), facts_atts_s) ctxt =
    1.31 +fun local_note_qualified kind facts ctxt =
    1.32    ctxt
    1.33    |> ProofContext.qualified_names
    1.34 -  |> yield_singleton (ProofContext.note_thmss_i kind) ((b, atts), facts_atts_s)
    1.35 +  |> ProofContext.note_thmss_i kind facts
    1.36    ||> ProofContext.restore_naming ctxt;
    1.37  
    1.38  
    1.39 @@ -1010,7 +1010,7 @@
    1.40    | activate_elem _ is_ext (Notes (kind, facts)) (ctxt, mode) =
    1.41        let
    1.42          val facts' = Attrib.map_facts (Attrib.attribute_i (ProofContext.theory_of ctxt)) facts;
    1.43 -        val (res, ctxt') = ctxt |> fold_map (local_note_qualified kind) facts';
    1.44 +        val (res, ctxt') = ctxt |> local_note_qualified kind facts';
    1.45        in (if is_ext then (map (#1 o #1) facts' ~~ map #2 res) else [], (ctxt', mode)) end;
    1.46  
    1.47  fun activate_elems ax_in_ctxt (((name, ps), mode), elems) ctxt =
    1.48 @@ -1696,7 +1696,8 @@
    1.49                 (Attrib.attribute_i thy) insts prems eqns exp;
    1.50        in
    1.51          thy
    1.52 -        |> fold (snd oo global_note_qualified kind) args'
    1.53 +        |> global_note_qualified kind args'
    1.54 +        |> snd
    1.55        end;
    1.56    in fold activate regs thy end;
    1.57  
    1.58 @@ -2106,7 +2107,8 @@
    1.59                   (attrib thy_ctxt) insts prems eqns exp;
    1.60          in 
    1.61            thy_ctxt
    1.62 -          |> fold (snd oo note kind) facts'
    1.63 +          |> note kind facts'
    1.64 +          |> snd
    1.65          end
    1.66        | activate_elem _ _ _ _ _ _ _ thy_ctxt = thy_ctxt;
    1.67  
    1.68 @@ -2128,7 +2130,7 @@
    1.69    in
    1.70      thy_ctxt''
    1.71      (* add equations as lemmas to context *)
    1.72 -    |> (fold2 o fold2) (fn attn => fn thm => snd o note Thm.lemmaK
    1.73 +    |> (fold2 o fold2) (fn attn => fn thm => snd o yield_singleton (note Thm.lemmaK)
    1.74           ((apsnd o map) (attrib thy_ctxt'') attn, [([Element.conclude_witness thm], [])]))
    1.75              (unflat eq_thms eq_attns) eq_thms
    1.76      (* add interpreted facts *)
    1.77 @@ -2383,7 +2385,8 @@
    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_qualified kind) facts'
    1.82 +                  |> global_note_qualified kind facts'
    1.83 +                  |> snd
    1.84                  end
    1.85                | activate_elem _ _ thy = thy;
    1.86