--- a/src/Pure/Isar/specification.ML Sat Sep 01 19:27:28 2012 +0200
+++ b/src/Pure/Isar/specification.ML Sat Sep 01 19:43:18 2012 +0200
@@ -395,8 +395,7 @@
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', Local_Theory.register_proofs (flat results) 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;