# HG changeset patch
# User wenzelm
# Date 1331654640 -3600
# Node ID 3c1787d469357d7b42569cc01c11e16df4de8458
# Parent  6b1c0a80a57a58c9c34f3eccb8a12fa64d73d209
suppress vacous notes elements, with subtle change of semantics: 'interpret' no longer pulls-in unnamed facts "by fact";

diff -r 6b1c0a80a57a -r 3c1787d46935 src/Pure/Isar/attrib.ML
--- a/src/Pure/Isar/attrib.ML	Tue Mar 13 16:56:56 2012 +0100
+++ b/src/Pure/Isar/attrib.ML	Tue Mar 13 17:04:00 2012 +0100
@@ -283,7 +283,8 @@
           else if null decls' then [((b, []), fact')]
           else [(empty_binding, decls'), ((b, []), fact')];
       in (facts', context') end)
-  |> fst |> flat |> map (apsnd (map (apfst single)));
+  |> fst |> flat |> map (apsnd (map (apfst single)))
+  |> filter_out (fn (b, fact) => is_empty_binding b andalso forall (null o #2) fact);
 
 end;
 
diff -r 6b1c0a80a57a -r 3c1787d46935 src/Pure/Isar/locale.ML
--- a/src/Pure/Isar/locale.ML	Tue Mar 13 16:56:56 2012 +0100
+++ b/src/Pure/Isar/locale.ML	Tue Mar 13 17:04:00 2012 +0100
@@ -533,21 +533,22 @@
 
 (* Theorems *)
 
-fun add_thmss loc kind facts ctxt =
-  ctxt
-  |> Proof_Context.note_thmss kind
-    (Attrib.map_facts (map (Attrib.attribute_i (Proof_Context.theory_of ctxt))) facts)
-  |> snd
-  |> Proof_Context.background_theory
-    ((change_locale loc o apfst o apsnd) (cons ((kind, facts), serial ())) #>
-      (* Registrations *)
-      (fn thy => fold_rev (fn (_, morph) =>
-            let
-              val facts' = facts
-                |> Element.transform_facts morph
-                |> Attrib.map_facts (map (Attrib.attribute_i thy));
-            in snd o Global_Theory.note_thmss kind facts' end)
-        (registrations_of (Context.Theory thy) loc) thy));
+fun add_thmss _ _ [] ctxt = ctxt
+  | add_thmss loc kind facts ctxt =
+      ctxt
+      |> Proof_Context.note_thmss kind
+        (Attrib.map_facts (map (Attrib.attribute_i (Proof_Context.theory_of ctxt))) facts)
+      |> snd
+      |> Proof_Context.background_theory
+        ((change_locale loc o apfst o apsnd) (cons ((kind, facts), serial ())) #>
+          (* Registrations *)
+          (fn thy => fold_rev (fn (_, morph) =>
+                let
+                  val facts' = facts
+                    |> Element.transform_facts morph
+                    |> Attrib.map_facts (map (Attrib.attribute_i thy));
+                in snd o Global_Theory.note_thmss kind facts' end)
+            (registrations_of (Context.Theory thy) loc) thy));
 
 
 (* Declarations *)