--- 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;