src/Pure/Isar/expression.ML

--- a/src/Pure/Isar/expression.ML	Tue Mar 13 13:31:26 2012 +0100
+++ b/src/Pure/Isar/expression.ML	Tue Mar 13 14:17:42 2012 +0100
@@ -858,7 +858,8 @@
 
     fun after_qed witss eqns =
       (Proof.map_context o Context.proof_map)
-        (note_eqns_register deps witss attrss eqns export export');
+        (note_eqns_register deps witss attrss eqns export export')
+      #> Proof.put_facts NONE;
   in
     state
     |> Element.witness_local_proof_eqs after_qed "interpret" propss eqns goal_ctxt int