# HG changeset patch
# User wenzelm
# Date 1321704170 -3600
# Node ID 41a768a431a60cf8cfc5b041f712d17037dbb1ee
# Parent  93499f36d59a94f5f464e967f1963b090a551549
do not store vacuous theorem specifications -- relevant for frugal local theory content;
tuned;

diff -r 93499f36d59a -r 41a768a431a6 src/Pure/Isar/attrib.ML
--- a/src/Pure/Isar/attrib.ML	Sat Nov 19 12:33:18 2011 +0100
+++ b/src/Pure/Isar/attrib.ML	Sat Nov 19 13:02:50 2011 +0100
@@ -9,6 +9,7 @@
   type src = Args.src
   type binding = binding * src list
   val empty_binding: binding
+  val is_empty_binding: binding -> bool
   val print_attributes: theory -> unit
   val intern: theory -> xstring -> string
   val intern_src: theory -> src -> src
@@ -60,7 +61,9 @@
 type src = Args.src;
 
 type binding = binding * src list;
+
 val empty_binding: binding = (Binding.empty, []);
+fun is_empty_binding ((b, srcs): binding) = Binding.is_empty b andalso null srcs;
 
 
 
diff -r 93499f36d59a -r 41a768a431a6 src/Pure/Isar/element.ML
--- a/src/Pure/Isar/element.ML	Sat Nov 19 12:33:18 2011 +0100
+++ b/src/Pure/Isar/element.ML	Sat Nov 19 13:02:50 2011 +0100
@@ -119,7 +119,7 @@
         map (fn y => Pretty.block [Pretty.str "  ", Pretty.keyword sep, Pretty.brk 1, y]) ys;
 
 fun pretty_name_atts ctxt (b, atts) sep =
-  if Binding.is_empty b andalso null atts then []
+  if Attrib.is_empty_binding (b, atts) then []
   else
     [Pretty.block (Pretty.breaks
       (Binding.pretty b :: Attrib.pretty_attribs ctxt atts @ [Pretty.str sep]))];
diff -r 93499f36d59a -r 41a768a431a6 src/Pure/Isar/specification.ML
--- a/src/Pure/Isar/specification.ML	Sat Nov 19 12:33:18 2011 +0100
+++ b/src/Pure/Isar/specification.ML	Sat Nov 19 13:02:50 2011 +0100
@@ -375,23 +375,23 @@
     val atts = more_atts @ map attrib raw_atts;
 
     fun after_qed' results goal_ctxt' =
-      let val results' =
-        burrow (map Goal.norm_result o Proof_Context.export goal_ctxt' lthy) results
-      in
-        lthy
-        |> Local_Theory.notes_kind kind
-          (map2 (fn (a, _) => fn ths => (a, [(ths, [])])) stmt results')
-        |> (fn (res, lthy') =>
-          if Binding.is_empty name andalso null atts then
+      let
+        val results' = burrow (map Goal.norm_result o Proof_Context.export goal_ctxt' lthy) results;
+        val (res, lthy') =
+          if forall (Attrib.is_empty_binding o fst) stmt then (map (pair "") results', lthy)
+          else
+            Local_Theory.notes_kind kind
+              (map2 (fn (b, _) => fn ths => (b, [(ths, [])])) stmt results') lthy;
+        val lthy'' =
+          if Attrib.is_empty_binding (name, atts) then
             (Proof_Display.print_results int lthy' ((kind, ""), res); lthy')
           else
             let
-              val ([(res_name, _)], lthy'') = lthy'
-                |> Local_Theory.notes_kind kind [((name, atts), [(maps #2 res, [])])];
+              val ([(res_name, _)], lthy'') =
+                Local_Theory.notes_kind kind [((name, atts), [(maps #2 res, [])])] lthy';
               val _ = Proof_Display.print_results int lthy' ((kind, res_name), res);
-            in lthy'' end)
-        |> after_qed results'
-      end;
+            in lthy'' end;
+      in after_qed results' lthy'' end;
   in
     goal_ctxt
     |> Proof_Context.note_thmss "" [((Binding.name Auto_Bind.assmsN, []), [(prems, [])])]