# HG changeset patch
# User wenzelm
# Date 1331644662 -3600
# Node ID 58110c1e02bcd35412002ad319c0f60ee0dd9dc0
# Parent  1570b30ee040d2ccd55ca22185642297917a018c
refined 'interpret': reset facts ("this") and print_result, which merely consist of internal / protected statement;

diff -r 1570b30ee040 -r 58110c1e02bc src/Pure/Isar/element.ML
--- a/src/Pure/Isar/element.ML	Tue Mar 13 13:31:26 2012 +0100
+++ b/src/Pure/Isar/element.ML	Tue Mar 13 14:17:42 2012 +0100
@@ -288,8 +288,8 @@
 
 fun proof_local cmd goal_ctxt int after_qed' propss =
   Proof.map_context (K goal_ctxt) #>
-  Proof.local_goal (Proof_Display.print_results Isabelle_Markup.state int) (K I)
-    Proof_Context.bind_propp_i cmd NONE after_qed' (map (pair Thm.empty_binding) propss);
+  Proof.local_goal (K (K ())) (K I) Proof_Context.bind_propp_i cmd NONE
+    after_qed' (map (pair Thm.empty_binding) propss);
 
 in
 
diff -r 1570b30ee040 -r 58110c1e02bc 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