# HG changeset patch # User wenzelm # Date 1320681623 -3600 # Node ID e29521ef9059999f9ccb40daed3ccb655985f2b8 # Parent bc0d50f8ae19670fd4f6242598fe5b8c74c437b4 tuned signature -- avoid spurious Thm.mixed_attribute; diff -r bc0d50f8ae19 -r e29521ef9059 src/Pure/Isar/attrib.ML --- a/src/Pure/Isar/attrib.ML Mon Nov 07 16:41:16 2011 +0100 +++ b/src/Pure/Isar/attrib.ML Mon Nov 07 17:00:23 2011 +0100 @@ -16,12 +16,12 @@ val defined: theory -> string -> bool val attribute: theory -> src -> attribute val attribute_i: theory -> src -> attribute - val map_specs: ('a -> 'att) -> + val map_specs: ('a list -> 'att list) -> (('c * 'a list) * 'b) list -> (('c * 'att list) * 'b) list - val map_facts: ('a -> 'att) -> + val map_facts: ('a list -> 'att list) -> (('c * 'a list) * ('d * 'a list) list) list -> (('c * 'att list) * ('d * 'att list) list) list - val map_facts_refs: ('a -> 'att) -> ('b -> 'fact) -> + val map_facts_refs: ('a list -> 'att list) -> ('b -> 'fact) -> (('c * 'a list) * ('b * 'a list) list) list -> (('c * 'att list) * ('fact * 'att list) list) list val eval_thms: Proof.context -> (Facts.ref * src list) list -> thm list @@ -127,9 +127,9 @@ (* attributed declarations *) -fun map_specs f = map (apfst (apsnd (map f))); +fun map_specs f = map (apfst (apsnd f)); -fun map_facts f = map (apfst (apsnd (map f)) o apsnd (map (apsnd (map f)))); +fun map_facts f = map (apfst (apsnd f) o apsnd (map (apsnd f))); fun map_facts_refs f g = map_facts f #> map (apsnd (map (apfst g))); @@ -137,7 +137,7 @@ fun eval_thms ctxt srcs = ctxt |> Proof_Context.note_thmss "" - (map_facts_refs (attribute (Proof_Context.theory_of ctxt)) (Proof_Context.get_fact ctxt) + (map_facts_refs (map (attribute (Proof_Context.theory_of ctxt))) (Proof_Context.get_fact ctxt) [((Binding.empty, []), srcs)]) |> fst |> maps snd; diff -r bc0d50f8ae19 -r e29521ef9059 src/Pure/Isar/element.ML --- a/src/Pure/Isar/element.ML Mon Nov 07 16:41:16 2011 +0100 +++ b/src/Pure/Isar/element.ML Mon Nov 07 17:00:23 2011 +0100 @@ -481,7 +481,8 @@ fun generic_note_thmss kind facts context = let - val facts' = Attrib.map_facts (Attrib.attribute_i (Context.theory_of context)) facts; + val facts' = + Attrib.map_facts (map (Attrib.attribute_i (Context.theory_of context))) facts; in context |> Context.mapping_result (Global_Theory.note_thmss kind facts') @@ -492,14 +493,16 @@ | init (Constrains _) = I | init (Assumes asms) = Context.map_proof (fn ctxt => let - val asms' = Attrib.map_specs (Attrib.attribute_i (Proof_Context.theory_of ctxt)) asms; + val asms' = + Attrib.map_specs (map (Attrib.attribute_i (Proof_Context.theory_of ctxt))) asms; val (_, ctxt') = ctxt |> fold Variable.auto_fixes (maps (map #1 o #2) asms') |> Proof_Context.add_assms_i Assumption.assume_export asms'; in ctxt' end) | init (Defines defs) = Context.map_proof (fn ctxt => let - val defs' = Attrib.map_specs (Attrib.attribute_i (Proof_Context.theory_of ctxt)) defs; + val defs' = + Attrib.map_specs (map (Attrib.attribute_i (Proof_Context.theory_of ctxt))) defs; val asms = defs' |> map (fn ((name, atts), (t, ps)) => let val ((c, _), t') = Local_Defs.cert_def ctxt t (* FIXME adapt ps? *) in (t', ((Thm.def_binding_optional (Binding.name c) name, atts), [(t', ps)])) end); diff -r bc0d50f8ae19 -r e29521ef9059 src/Pure/Isar/generic_target.ML --- a/src/Pure/Isar/generic_target.ML Mon Nov 07 16:41:16 2011 +0100 +++ b/src/Pure/Isar/generic_target.ML Mon Nov 07 17:00:23 2011 +0100 @@ -156,7 +156,7 @@ in lthy |> target_notes kind global_facts local_facts - |> Proof_Context.note_thmss kind (Attrib.map_facts (Attrib.attribute_i thy) local_facts) + |> Proof_Context.note_thmss kind (Attrib.map_facts (map (Attrib.attribute_i thy)) local_facts) end; @@ -212,7 +212,7 @@ fun theory_notes kind global_facts lthy = let val thy = Proof_Context.theory_of lthy; - val global_facts' = Attrib.map_facts (Attrib.attribute_i thy) global_facts; + val global_facts' = Attrib.map_facts (map (Attrib.attribute_i thy)) global_facts; in lthy |> Local_Theory.background_theory (Global_Theory.note_thmss kind global_facts' #> snd) diff -r bc0d50f8ae19 -r e29521ef9059 src/Pure/Isar/locale.ML --- a/src/Pure/Isar/locale.ML Mon Nov 07 16:41:16 2011 +0100 +++ b/src/Pure/Isar/locale.ML Mon Nov 07 17:00:23 2011 +0100 @@ -562,8 +562,9 @@ (* Registrations *) (fn thy => fold_rev (fn (_, morph) => let - val args'' = snd args' |> Element.facts_map (Element.transform_ctxt morph) |> - Attrib.map_facts (Attrib.attribute_i thy) + val args'' = snd args' + |> Element.facts_map (Element.transform_ctxt morph) + |> Attrib.map_facts (map (Attrib.attribute_i thy)); in Global_Theory.note_thmss kind args'' #> snd end) (registrations_of (Context.Theory thy) loc) thy)) in ctxt'' end; diff -r bc0d50f8ae19 -r e29521ef9059 src/Pure/Isar/named_target.ML --- a/src/Pure/Isar/named_target.ML Mon Nov 07 16:41:16 2011 +0100 +++ b/src/Pure/Isar/named_target.ML Mon Nov 07 17:00:23 2011 +0100 @@ -117,7 +117,7 @@ fun locale_notes locale kind global_facts local_facts lthy = let - val global_facts' = Attrib.map_facts (K (Thm.mixed_attribute I)) global_facts; + val global_facts' = Attrib.map_facts (K []) global_facts; val local_facts' = Element.facts_map (Element.transform_ctxt (Local_Theory.target_morphism lthy)) local_facts; in diff -r bc0d50f8ae19 -r e29521ef9059 src/Pure/Isar/obtain.ML --- a/src/Pure/Isar/obtain.ML Mon Nov 07 16:41:16 2011 +0100 +++ b/src/Pure/Isar/obtain.ML Mon Nov 07 17:00:23 2011 +0100 @@ -126,7 +126,7 @@ val (proppss, asms_ctxt) = prep_propp (map snd raw_asms) fix_ctxt; val ((_, bind_ctxt), _) = Proof_Context.bind_propp_i proppss asms_ctxt; val asm_props = maps (map fst) proppss; - val asms = map fst (Attrib.map_specs (prep_att thy) raw_asms) ~~ proppss; + val asms = map fst (Attrib.map_specs (map (prep_att thy)) raw_asms) ~~ proppss; (*obtain parms*) val (Ts, parms_ctxt) = fold_map Proof_Context.inferred_param xs' asms_ctxt; diff -r bc0d50f8ae19 -r e29521ef9059 src/Pure/Isar/proof.ML --- a/src/Pure/Isar/proof.ML Mon Nov 07 16:41:16 2011 +0100 +++ b/src/Pure/Isar/proof.ML Mon Nov 07 17:00:23 2011 +0100 @@ -593,7 +593,7 @@ fun gen_assume asm prep_att exp args state = state |> assert_forward - |> map_context_result (asm exp (Attrib.map_specs (prep_att (theory_of state)) args)) + |> map_context_result (asm exp (Attrib.map_specs (map (prep_att (theory_of state))) args)) |> these_factss [] |> #2; in @@ -665,7 +665,9 @@ state |> assert_forward |> map_context_result (Proof_Context.note_thmss "" - (Attrib.map_facts_refs (prep_atts (theory_of state)) (prep_fact (context_of state)) args)) + (Attrib.map_facts_refs + (map (prep_atts (theory_of state))) + (prep_fact (context_of state)) args)) |> these_factss (more_facts state) ||> opt_chain |> opt_result; @@ -690,12 +692,12 @@ local -fun gen_using f g prep_atts prep_fact args state = +fun gen_using f g prep_att prep_fact args state = state |> assert_backward |> map_context_result (Proof_Context.note_thmss "" - (Attrib.map_facts_refs (prep_atts (theory_of state)) (prep_fact (context_of state)) + (Attrib.map_facts_refs (map (prep_att (theory_of state))) (prep_fact (context_of state)) (no_binding args))) |> (fn (named_facts, state') => state' |> map_goal I (fn (statement, _, using, goal, before_qed, after_qed) => @@ -916,7 +918,7 @@ let val thy = theory_of state; val ((names, attss), propp) = - Attrib.map_specs (prep_att thy) stmt |> split_list |>> split_list; + Attrib.map_specs (map (prep_att thy)) stmt |> split_list |>> split_list; fun after_qed' results = local_results ((names ~~ attss) ~~ results) diff -r bc0d50f8ae19 -r e29521ef9059 src/Pure/Isar/specification.ML --- a/src/Pure/Isar/specification.ML Mon Nov 07 16:41:16 2011 +0100 +++ b/src/Pure/Isar/specification.ML Mon Nov 07 17:00:23 2011 +0100 @@ -307,7 +307,7 @@ let val (propp, elems_ctxt) = prep_stmt elems (map snd shows) ctxt; val prems = Assumption.local_prems_of elems_ctxt ctxt; - val stmt = Attrib.map_specs prep_att (map fst shows ~~ propp); + val stmt = Attrib.map_specs (map prep_att) (map fst shows ~~ propp); val goal_ctxt = (fold o fold) (Variable.auto_fixes o fst) propp elems_ctxt; in ((prems, stmt, NONE), goal_ctxt) end | Element.Obtains obtains =>