suppress vacous notes elements, with subtle change of semantics: 'interpret' no longer pulls-in unnamed facts "by fact";
authorwenzelm
Tue Mar 13 17:04:00 2012 +0100 (2012-03-13)
changeset 469063c1787d46935
parent 46905 6b1c0a80a57a
child 46908 3553cb65c66c
suppress vacous notes elements, with subtle change of semantics: 'interpret' no longer pulls-in unnamed facts "by fact";
src/Pure/Isar/attrib.ML
src/Pure/Isar/locale.ML
     1.1 --- a/src/Pure/Isar/attrib.ML	Tue Mar 13 16:56:56 2012 +0100
     1.2 +++ b/src/Pure/Isar/attrib.ML	Tue Mar 13 17:04:00 2012 +0100
     1.3 @@ -283,7 +283,8 @@
     1.4            else if null decls' then [((b, []), fact')]
     1.5            else [(empty_binding, decls'), ((b, []), fact')];
     1.6        in (facts', context') end)
     1.7 -  |> fst |> flat |> map (apsnd (map (apfst single)));
     1.8 +  |> fst |> flat |> map (apsnd (map (apfst single)))
     1.9 +  |> filter_out (fn (b, fact) => is_empty_binding b andalso forall (null o #2) fact);
    1.10  
    1.11  end;
    1.12  
     2.1 --- a/src/Pure/Isar/locale.ML	Tue Mar 13 16:56:56 2012 +0100
     2.2 +++ b/src/Pure/Isar/locale.ML	Tue Mar 13 17:04:00 2012 +0100
     2.3 @@ -533,21 +533,22 @@
     2.4  
     2.5  (* Theorems *)
     2.6  
     2.7 -fun add_thmss loc kind facts ctxt =
     2.8 -  ctxt
     2.9 -  |> Proof_Context.note_thmss kind
    2.10 -    (Attrib.map_facts (map (Attrib.attribute_i (Proof_Context.theory_of ctxt))) facts)
    2.11 -  |> snd
    2.12 -  |> Proof_Context.background_theory
    2.13 -    ((change_locale loc o apfst o apsnd) (cons ((kind, facts), serial ())) #>
    2.14 -      (* Registrations *)
    2.15 -      (fn thy => fold_rev (fn (_, morph) =>
    2.16 -            let
    2.17 -              val facts' = facts
    2.18 -                |> Element.transform_facts morph
    2.19 -                |> Attrib.map_facts (map (Attrib.attribute_i thy));
    2.20 -            in snd o Global_Theory.note_thmss kind facts' end)
    2.21 -        (registrations_of (Context.Theory thy) loc) thy));
    2.22 +fun add_thmss _ _ [] ctxt = ctxt
    2.23 +  | add_thmss loc kind facts ctxt =
    2.24 +      ctxt
    2.25 +      |> Proof_Context.note_thmss kind
    2.26 +        (Attrib.map_facts (map (Attrib.attribute_i (Proof_Context.theory_of ctxt))) facts)
    2.27 +      |> snd
    2.28 +      |> Proof_Context.background_theory
    2.29 +        ((change_locale loc o apfst o apsnd) (cons ((kind, facts), serial ())) #>
    2.30 +          (* Registrations *)
    2.31 +          (fn thy => fold_rev (fn (_, morph) =>
    2.32 +                let
    2.33 +                  val facts' = facts
    2.34 +                    |> Element.transform_facts morph
    2.35 +                    |> Attrib.map_facts (map (Attrib.attribute_i thy));
    2.36 +                in snd o Global_Theory.note_thmss kind facts' end)
    2.37 +            (registrations_of (Context.Theory thy) loc) thy));
    2.38  
    2.39  
    2.40  (* Declarations *)