tuned signature -- avoid spurious Thm.mixed_attribute;
authorwenzelm
Mon Nov 07 17:00:23 2011 +0100 (2011-11-07 ago)
changeset 45390e29521ef9059
parent 45389 bc0d50f8ae19
child 45391 30f6617c9986
tuned signature -- avoid spurious Thm.mixed_attribute;
src/Pure/Isar/attrib.ML
src/Pure/Isar/element.ML
src/Pure/Isar/generic_target.ML
src/Pure/Isar/locale.ML
src/Pure/Isar/named_target.ML
src/Pure/Isar/obtain.ML
src/Pure/Isar/proof.ML
src/Pure/Isar/specification.ML
     1.1 --- a/src/Pure/Isar/attrib.ML	Mon Nov 07 16:41:16 2011 +0100
     1.2 +++ b/src/Pure/Isar/attrib.ML	Mon Nov 07 17:00:23 2011 +0100
     1.3 @@ -16,12 +16,12 @@
     1.4    val defined: theory -> string -> bool
     1.5    val attribute: theory -> src -> attribute
     1.6    val attribute_i: theory -> src -> attribute
     1.7 -  val map_specs: ('a -> 'att) ->
     1.8 +  val map_specs: ('a list -> 'att list) ->
     1.9      (('c * 'a list) * 'b) list -> (('c * 'att list) * 'b) list
    1.10 -  val map_facts: ('a -> 'att) ->
    1.11 +  val map_facts: ('a list -> 'att list) ->
    1.12      (('c * 'a list) * ('d * 'a list) list) list ->
    1.13      (('c * 'att list) * ('d * 'att list) list) list
    1.14 -  val map_facts_refs: ('a -> 'att) -> ('b -> 'fact) ->
    1.15 +  val map_facts_refs: ('a list -> 'att list) -> ('b -> 'fact) ->
    1.16      (('c * 'a list) * ('b * 'a list) list) list ->
    1.17      (('c * 'att list) * ('fact * 'att list) list) list
    1.18    val eval_thms: Proof.context -> (Facts.ref * src list) list -> thm list
    1.19 @@ -127,9 +127,9 @@
    1.20  
    1.21  (* attributed declarations *)
    1.22  
    1.23 -fun map_specs f = map (apfst (apsnd (map f)));
    1.24 +fun map_specs f = map (apfst (apsnd f));
    1.25  
    1.26 -fun map_facts f = map (apfst (apsnd (map f)) o apsnd (map (apsnd (map f))));
    1.27 +fun map_facts f = map (apfst (apsnd f) o apsnd (map (apsnd f)));
    1.28  fun map_facts_refs f g = map_facts f #> map (apsnd (map (apfst g)));
    1.29  
    1.30  
    1.31 @@ -137,7 +137,7 @@
    1.32  
    1.33  fun eval_thms ctxt srcs = ctxt
    1.34    |> Proof_Context.note_thmss ""
    1.35 -    (map_facts_refs (attribute (Proof_Context.theory_of ctxt)) (Proof_Context.get_fact ctxt)
    1.36 +    (map_facts_refs (map (attribute (Proof_Context.theory_of ctxt))) (Proof_Context.get_fact ctxt)
    1.37        [((Binding.empty, []), srcs)])
    1.38    |> fst |> maps snd;
    1.39  
     2.1 --- a/src/Pure/Isar/element.ML	Mon Nov 07 16:41:16 2011 +0100
     2.2 +++ b/src/Pure/Isar/element.ML	Mon Nov 07 17:00:23 2011 +0100
     2.3 @@ -481,7 +481,8 @@
     2.4  
     2.5  fun generic_note_thmss kind facts context =
     2.6    let
     2.7 -    val facts' = Attrib.map_facts (Attrib.attribute_i (Context.theory_of context)) facts;
     2.8 +    val facts' =
     2.9 +      Attrib.map_facts (map (Attrib.attribute_i (Context.theory_of context))) facts;
    2.10    in
    2.11      context |> Context.mapping_result
    2.12        (Global_Theory.note_thmss kind facts')
    2.13 @@ -492,14 +493,16 @@
    2.14    | init (Constrains _) = I
    2.15    | init (Assumes asms) = Context.map_proof (fn ctxt =>
    2.16        let
    2.17 -        val asms' = Attrib.map_specs (Attrib.attribute_i (Proof_Context.theory_of ctxt)) asms;
    2.18 +        val asms' =
    2.19 +          Attrib.map_specs (map (Attrib.attribute_i (Proof_Context.theory_of ctxt))) asms;
    2.20          val (_, ctxt') = ctxt
    2.21            |> fold Variable.auto_fixes (maps (map #1 o #2) asms')
    2.22            |> Proof_Context.add_assms_i Assumption.assume_export asms';
    2.23        in ctxt' end)
    2.24    | init (Defines defs) = Context.map_proof (fn ctxt =>
    2.25        let
    2.26 -        val defs' = Attrib.map_specs (Attrib.attribute_i (Proof_Context.theory_of ctxt)) defs;
    2.27 +        val defs' =
    2.28 +          Attrib.map_specs (map (Attrib.attribute_i (Proof_Context.theory_of ctxt))) defs;
    2.29          val asms = defs' |> map (fn ((name, atts), (t, ps)) =>
    2.30              let val ((c, _), t') = Local_Defs.cert_def ctxt t  (* FIXME adapt ps? *)
    2.31              in (t', ((Thm.def_binding_optional (Binding.name c) name, atts), [(t', ps)])) end);
     3.1 --- a/src/Pure/Isar/generic_target.ML	Mon Nov 07 16:41:16 2011 +0100
     3.2 +++ b/src/Pure/Isar/generic_target.ML	Mon Nov 07 17:00:23 2011 +0100
     3.3 @@ -156,7 +156,7 @@
     3.4    in
     3.5      lthy
     3.6      |> target_notes kind global_facts local_facts
     3.7 -    |> Proof_Context.note_thmss kind (Attrib.map_facts (Attrib.attribute_i thy) local_facts)
     3.8 +    |> Proof_Context.note_thmss kind (Attrib.map_facts (map (Attrib.attribute_i thy)) local_facts)
     3.9    end;
    3.10  
    3.11  
    3.12 @@ -212,7 +212,7 @@
    3.13  fun theory_notes kind global_facts lthy =
    3.14    let
    3.15      val thy = Proof_Context.theory_of lthy;
    3.16 -    val global_facts' = Attrib.map_facts (Attrib.attribute_i thy) global_facts;
    3.17 +    val global_facts' = Attrib.map_facts (map (Attrib.attribute_i thy)) global_facts;
    3.18    in
    3.19      lthy
    3.20      |> Local_Theory.background_theory (Global_Theory.note_thmss kind global_facts' #> snd)
     4.1 --- a/src/Pure/Isar/locale.ML	Mon Nov 07 16:41:16 2011 +0100
     4.2 +++ b/src/Pure/Isar/locale.ML	Mon Nov 07 17:00:23 2011 +0100
     4.3 @@ -562,8 +562,9 @@
     4.4        (* Registrations *)
     4.5        (fn thy => fold_rev (fn (_, morph) =>
     4.6              let
     4.7 -              val args'' = snd args' |> Element.facts_map (Element.transform_ctxt morph) |>
     4.8 -                Attrib.map_facts (Attrib.attribute_i thy)
     4.9 +              val args'' = snd args'
    4.10 +                |> Element.facts_map (Element.transform_ctxt morph)
    4.11 +                |> Attrib.map_facts (map (Attrib.attribute_i thy));
    4.12              in Global_Theory.note_thmss kind args'' #> snd end)
    4.13          (registrations_of (Context.Theory thy) loc) thy))
    4.14    in ctxt'' end;
     5.1 --- a/src/Pure/Isar/named_target.ML	Mon Nov 07 16:41:16 2011 +0100
     5.2 +++ b/src/Pure/Isar/named_target.ML	Mon Nov 07 17:00:23 2011 +0100
     5.3 @@ -117,7 +117,7 @@
     5.4  
     5.5  fun locale_notes locale kind global_facts local_facts lthy =
     5.6    let
     5.7 -    val global_facts' = Attrib.map_facts (K (Thm.mixed_attribute I)) global_facts;
     5.8 +    val global_facts' = Attrib.map_facts (K []) global_facts;
     5.9      val local_facts' = Element.facts_map
    5.10        (Element.transform_ctxt (Local_Theory.target_morphism lthy)) local_facts;
    5.11    in
     6.1 --- a/src/Pure/Isar/obtain.ML	Mon Nov 07 16:41:16 2011 +0100
     6.2 +++ b/src/Pure/Isar/obtain.ML	Mon Nov 07 17:00:23 2011 +0100
     6.3 @@ -126,7 +126,7 @@
     6.4      val (proppss, asms_ctxt) = prep_propp (map snd raw_asms) fix_ctxt;
     6.5      val ((_, bind_ctxt), _) = Proof_Context.bind_propp_i proppss asms_ctxt;
     6.6      val asm_props = maps (map fst) proppss;
     6.7 -    val asms = map fst (Attrib.map_specs (prep_att thy) raw_asms) ~~ proppss;
     6.8 +    val asms = map fst (Attrib.map_specs (map (prep_att thy)) raw_asms) ~~ proppss;
     6.9  
    6.10      (*obtain parms*)
    6.11      val (Ts, parms_ctxt) = fold_map Proof_Context.inferred_param xs' asms_ctxt;
     7.1 --- a/src/Pure/Isar/proof.ML	Mon Nov 07 16:41:16 2011 +0100
     7.2 +++ b/src/Pure/Isar/proof.ML	Mon Nov 07 17:00:23 2011 +0100
     7.3 @@ -593,7 +593,7 @@
     7.4  fun gen_assume asm prep_att exp args state =
     7.5    state
     7.6    |> assert_forward
     7.7 -  |> map_context_result (asm exp (Attrib.map_specs (prep_att (theory_of state)) args))
     7.8 +  |> map_context_result (asm exp (Attrib.map_specs (map (prep_att (theory_of state))) args))
     7.9    |> these_factss [] |> #2;
    7.10  
    7.11  in
    7.12 @@ -665,7 +665,9 @@
    7.13    state
    7.14    |> assert_forward
    7.15    |> map_context_result (Proof_Context.note_thmss ""
    7.16 -    (Attrib.map_facts_refs (prep_atts (theory_of state)) (prep_fact (context_of state)) args))
    7.17 +    (Attrib.map_facts_refs
    7.18 +      (map (prep_atts (theory_of state)))
    7.19 +      (prep_fact (context_of state)) args))
    7.20    |> these_factss (more_facts state)
    7.21    ||> opt_chain
    7.22    |> opt_result;
    7.23 @@ -690,12 +692,12 @@
    7.24  
    7.25  local
    7.26  
    7.27 -fun gen_using f g prep_atts prep_fact args state =
    7.28 +fun gen_using f g prep_att prep_fact args state =
    7.29    state
    7.30    |> assert_backward
    7.31    |> map_context_result
    7.32      (Proof_Context.note_thmss ""
    7.33 -      (Attrib.map_facts_refs (prep_atts (theory_of state)) (prep_fact (context_of state))
    7.34 +      (Attrib.map_facts_refs (map (prep_att (theory_of state))) (prep_fact (context_of state))
    7.35          (no_binding args)))
    7.36    |> (fn (named_facts, state') =>
    7.37      state' |> map_goal I (fn (statement, _, using, goal, before_qed, after_qed) =>
    7.38 @@ -916,7 +918,7 @@
    7.39    let
    7.40      val thy = theory_of state;
    7.41      val ((names, attss), propp) =
    7.42 -      Attrib.map_specs (prep_att thy) stmt |> split_list |>> split_list;
    7.43 +      Attrib.map_specs (map (prep_att thy)) stmt |> split_list |>> split_list;
    7.44  
    7.45      fun after_qed' results =
    7.46        local_results ((names ~~ attss) ~~ results)
     8.1 --- a/src/Pure/Isar/specification.ML	Mon Nov 07 16:41:16 2011 +0100
     8.2 +++ b/src/Pure/Isar/specification.ML	Mon Nov 07 17:00:23 2011 +0100
     8.3 @@ -307,7 +307,7 @@
     8.4        let
     8.5          val (propp, elems_ctxt) = prep_stmt elems (map snd shows) ctxt;
     8.6          val prems = Assumption.local_prems_of elems_ctxt ctxt;
     8.7 -        val stmt = Attrib.map_specs prep_att (map fst shows ~~ propp);
     8.8 +        val stmt = Attrib.map_specs (map prep_att) (map fst shows ~~ propp);
     8.9          val goal_ctxt = (fold o fold) (Variable.auto_fixes o fst) propp elems_ctxt;
    8.10        in ((prems, stmt, NONE), goal_ctxt) end
    8.11    | Element.Obtains obtains =>