tuned;

--- a/src/Pure/Isar/locale.ML	Mon Nov 14 19:27:42 2011 +0100
+++ b/src/Pure/Isar/locale.ML	Mon Nov 14 20:25:22 2011 +0100
@@ -555,19 +555,19 @@
 
 (* Theorems *)
 
-fun add_thmss loc kind args ctxt =
+fun add_thmss loc kind facts ctxt =
   let
-    val (Notes args', ctxt') = Element.activate_i (Notes (kind, args)) ctxt;
+    val (Notes facts', ctxt') = Element.activate_i (Notes (kind, facts)) ctxt;
     val ctxt'' = ctxt' |> Proof_Context.background_theory
-     ((change_locale loc o apfst o apsnd) (cons (args', serial ()))
+     ((change_locale loc o apfst o apsnd) (cons (facts', serial ()))
         #>
       (* Registrations *)
       (fn thy => fold_rev (fn (_, morph) =>
             let
-              val args'' = snd args'
+              val facts'' = snd facts'
                 |> Element.facts_map (Element.transform_ctxt morph)
                 |> Attrib.map_facts (map (Attrib.attribute_i thy));
-            in Global_Theory.note_thmss kind args'' #> snd end)
+            in Global_Theory.note_thmss kind facts'' #> snd end)
         (registrations_of (Context.Theory thy) loc) thy))
   in ctxt'' end;