diff -r 528dec1c400b -r 6a909ee1c2f0 src/Pure/Isar/locale.ML
--- a/src/Pure/Isar/locale.ML	Wed Sep 02 10:30:02 2015 +0200
+++ b/src/Pure/Isar/locale.ML	Wed Sep 02 11:36:40 2015 +0200
@@ -573,19 +573,30 @@
 
 (* Theorems *)
 
-fun add_thmss _ _ [] ctxt = ctxt
-  | add_thmss loc kind facts ctxt =
-      let val facts0 = (map o apsnd o map o apfst o map) Thm.trim_context facts in
-        ctxt
-        |> Attrib.local_notes kind facts |> snd
-        |> Proof_Context.background_theory
-          ((change_locale loc o apfst o apsnd) (cons ((kind, facts0), serial ())) #>
-            (* Registrations *)
-            (fn thy =>
-              fold_rev (fn (_, morph) =>
-                snd o Attrib.global_notes kind (Attrib.transform_facts morph facts))
-              (registrations_of (Context.Theory thy) loc) thy))
-      end;
+local
+
+fun trim_context_facts facts =
+  (map o apsnd o map o apfst o map) Thm.trim_context facts;
+
+in
+
+fun add_thmss loc kind facts ctxt =
+  if null facts then ctxt
+  else
+    let
+      val notes = ((kind, trim_context_facts facts), serial ());
+      fun registrations thy =
+        fold_rev (fn (_, morph) =>
+            snd o Attrib.global_notes kind (Attrib.transform_facts morph facts))
+          (registrations_of (Context.Theory thy) loc) thy;
+    in
+      ctxt
+      |> Attrib.local_notes kind facts |> snd
+      |> Proof_Context.background_theory
+        ((change_locale loc o apfst o apsnd) (cons notes) #> registrations)
+    end;
+
+end;
 
 
 (* Declarations *)