simplified Locale.add_thmss, after partial evaluation of attributes;
authorwenzelm
Sat Nov 19 16:16:33 2011 +0100 (2011-11-19)
changeset 45589bb944d58ac19
parent 45588 5eb47a1e4ca7
child 45591 4e8899357971
simplified Locale.add_thmss, after partial evaluation of attributes;
src/Pure/Isar/expression.ML
src/Pure/Isar/locale.ML
     1.1 --- a/src/Pure/Isar/expression.ML	Sat Nov 19 15:34:37 2011 +0100
     1.2 +++ b/src/Pure/Isar/expression.ML	Sat Nov 19 16:16:33 2011 +0100
     1.3 @@ -895,7 +895,7 @@
     1.4        |> fst;  (* FIXME duplication to add_thmss *)
     1.5    in
     1.6      ctxt
     1.7 -    |> Locale.add_thmss target Thm.lemmaK facts
     1.8 +    |> Locale.add_thmss target Thm.lemmaK (Attrib.partial_evaluation ctxt facts)
     1.9      |> Proof_Context.background_theory (fold (fn ((dep, morph), wits) =>
    1.10        fn thy =>
    1.11          Locale.add_dependency target
     2.1 --- a/src/Pure/Isar/locale.ML	Sat Nov 19 15:34:37 2011 +0100
     2.2 +++ b/src/Pure/Isar/locale.ML	Sat Nov 19 16:16:33 2011 +0100
     2.3 @@ -343,7 +343,7 @@
     2.4    val empty = (Idtab.empty, Inttab.empty);
     2.5    val extend = I;
     2.6    fun merge ((reg1, mix1), (reg2, mix2)) : T =
     2.7 -    (Idtab.join (fn id => fn (r1 as (_, s1), r2 as (_, s2)) =>
     2.8 +    (Idtab.join (fn id => fn ((_, s1), (_, s2)) =>
     2.9          if s1 = s2 then raise Idtab.SAME else raise Idtab.DUP id) (reg1, reg2),
    2.10        merge_mixins (mix1, mix2))
    2.11      handle Idtab.DUP id =>
    2.12 @@ -557,20 +557,20 @@
    2.13  (* Theorems *)
    2.14  
    2.15  fun add_thmss loc kind facts ctxt =
    2.16 -  let
    2.17 -    val (Notes facts', ctxt') = Element.activate_i (Notes (kind, facts)) ctxt;
    2.18 -    val ctxt'' = ctxt' |> Proof_Context.background_theory
    2.19 -     ((change_locale loc o apfst o apsnd) (cons (facts', serial ()))
    2.20 -        #>
    2.21 +  ctxt
    2.22 +  |> Proof_Context.note_thmss kind
    2.23 +    (Attrib.map_facts (map (Attrib.attribute_i (Proof_Context.theory_of ctxt))) facts)
    2.24 +  |> snd
    2.25 +  |> Proof_Context.background_theory
    2.26 +    ((change_locale loc o apfst o apsnd) (cons ((kind, facts), serial ())) #>
    2.27        (* Registrations *)
    2.28        (fn thy => fold_rev (fn (_, morph) =>
    2.29              let
    2.30 -              val facts'' = snd facts'
    2.31 +              val facts' = facts
    2.32                  |> Element.facts_map (Element.transform_ctxt morph)
    2.33                  |> Attrib.map_facts (map (Attrib.attribute_i thy));
    2.34 -            in Global_Theory.note_thmss kind facts'' #> snd end)
    2.35 -        (registrations_of (Context.Theory thy) loc) thy))
    2.36 -  in ctxt'' end;
    2.37 +            in snd o Global_Theory.note_thmss kind facts' end)
    2.38 +        (registrations_of (Context.Theory thy) loc) thy));
    2.39  
    2.40  
    2.41  (* Declarations *)