# HG changeset patch
# User haftmann
# Date 1228143777 -3600
# Node ID df0cb410be355c3342b967b0b9c750f4814bef2c
# Parent  08004ce1b16773c12f5e206bab6df98e1e7ef7e1
Locale.*note* with conventional argument type

diff -r 08004ce1b167 -r df0cb410be35 src/Pure/Isar/locale.ML
--- a/src/Pure/Isar/locale.ML	Mon Dec 01 14:56:08 2008 +0100
+++ b/src/Pure/Isar/locale.ML	Mon Dec 01 16:02:57 2008 +0100
@@ -92,8 +92,8 @@
 
   (* Storing results *)
   val local_note_qualified: string ->
-    (Name.binding * attribute list) * (thm list * attribute list) list ->
-    Proof.context -> (string * thm list) * Proof.context
+    ((Name.binding * attribute list) * (thm list * attribute list) list) list ->
+    Proof.context -> (string * thm list) list * Proof.context
   val add_thmss: string -> string -> (Attrib.binding * (thm list * Attrib.src list) list) list ->
     Proof.context -> Proof.context
   val add_type_syntax: string -> declaration -> Proof.context -> Proof.context
@@ -134,18 +134,18 @@
 fun merge_alists eq xs = merge_lists (eq_fst eq) xs;
 
 
-(* auxiliary: noting with structured name bindings *)
-
-fun global_note_qualified kind ((b, atts), facts_atts_s) thy =
+(* auxiliary: noting name bindings with qualified base names *)
+
+fun global_note_qualified kind facts thy =
   thy
   |> Sign.qualified_names
-  |> yield_singleton (PureThy.note_thmss kind) ((b, atts), facts_atts_s)
+  |> PureThy.note_thmss kind facts
   ||> Sign.restore_naming thy;
 
-fun local_note_qualified kind ((b, atts), facts_atts_s) ctxt =
+fun local_note_qualified kind facts ctxt =
   ctxt
   |> ProofContext.qualified_names
-  |> yield_singleton (ProofContext.note_thmss_i kind) ((b, atts), facts_atts_s)
+  |> ProofContext.note_thmss_i kind facts
   ||> ProofContext.restore_naming ctxt;
 
 
@@ -1010,7 +1010,7 @@
   | activate_elem _ is_ext (Notes (kind, facts)) (ctxt, mode) =
       let
         val facts' = Attrib.map_facts (Attrib.attribute_i (ProofContext.theory_of ctxt)) facts;
-        val (res, ctxt') = ctxt |> fold_map (local_note_qualified kind) facts';
+        val (res, ctxt') = ctxt |> local_note_qualified kind facts';
       in (if is_ext then (map (#1 o #1) facts' ~~ map #2 res) else [], (ctxt', mode)) end;
 
 fun activate_elems ax_in_ctxt (((name, ps), mode), elems) ctxt =
@@ -1696,7 +1696,8 @@
                (Attrib.attribute_i thy) insts prems eqns exp;
       in
         thy
-        |> fold (snd oo global_note_qualified kind) args'
+        |> global_note_qualified kind args'
+        |> snd
       end;
   in fold activate regs thy end;
 
@@ -2106,7 +2107,8 @@
                  (attrib thy_ctxt) insts prems eqns exp;
         in 
           thy_ctxt
-          |> fold (snd oo note kind) facts'
+          |> note kind facts'
+          |> snd
         end
       | activate_elem _ _ _ _ _ _ _ thy_ctxt = thy_ctxt;
 
@@ -2128,7 +2130,7 @@
   in
     thy_ctxt''
     (* add equations as lemmas to context *)
-    |> (fold2 o fold2) (fn attn => fn thm => snd o note Thm.lemmaK
+    |> (fold2 o fold2) (fn attn => fn thm => snd o yield_singleton (note Thm.lemmaK)
          ((apsnd o map) (attrib thy_ctxt'') attn, [([Element.conclude_witness thm], [])]))
             (unflat eq_thms eq_attns) eq_thms
     (* add interpreted facts *)
@@ -2383,7 +2385,8 @@
                     |> (map o apfst o apfst) (name_morph phi_name param_prfx);
                 in
                   thy
-                  |> fold (snd oo global_note_qualified kind) facts'
+                  |> global_note_qualified kind facts'
+                  |> snd
                 end
               | activate_elem _ _ thy = thy;
 
diff -r 08004ce1b167 -r df0cb410be35 src/Pure/Isar/new_locale.ML
--- a/src/Pure/Isar/new_locale.ML	Mon Dec 01 14:56:08 2008 +0100
+++ b/src/Pure/Isar/new_locale.ML	Mon Dec 01 16:02:57 2008 +0100
@@ -295,7 +295,7 @@
   | init_elem (Notes (kind, facts)) ctxt =
       let
         val facts' = Attrib.map_facts (Attrib.attribute_i (ProofContext.theory_of ctxt)) facts
-      in fold (fn args => Locale.local_note_qualified kind args #> snd) facts' ctxt end
+      in Locale.local_note_qualified kind facts' ctxt |> snd end
 
 fun cons_elem false (Notes notes) elems = elems
   | cons_elem _ elem elems = elem :: elems