# HG changeset patch
# User wenzelm
# Date 1346444706 -7200
# Node ID be6d4e8307c802f9fe59e5b613787e2d8fd972ba
# Parent  2924a83a4a0b47f6a63f95e4b4af120267af4099
always register proofs, even for empty binding;

diff -r 2924a83a4a0b -r be6d4e8307c8 src/Pure/Isar/specification.ML
--- a/src/Pure/Isar/specification.ML	Fri Aug 31 22:24:14 2012 +0200
+++ b/src/Pure/Isar/specification.ML	Fri Aug 31 22:25:06 2012 +0200
@@ -395,7 +395,8 @@
       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)
+          if forall (Attrib.is_empty_binding o fst) stmt
+          then (map (pair "") results', Local_Theory.register_proofs (flat results) lthy)
           else
             Local_Theory.notes_kind kind
               (map2 (fn (b, _) => fn ths => (b, [(ths, [])])) stmt results') lthy;