do not store vacuous theorem specifications -- relevant for frugal local theory content;
tuned;
--- 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;
--- 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]))];
--- 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, [])])]