tuned signature -- avoid spurious Thm.mixed_attribute;

--- 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;
 

--- 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);

--- 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)

--- 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;

--- 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

--- 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;

--- 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)

--- 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 =>