1.1 --- a/src/Pure/Isar/element.ML	Tue Mar 13 13:31:26 2012 +0100
     1.2 +++ b/src/Pure/Isar/element.ML	Tue Mar 13 14:17:42 2012 +0100
     1.3 @@ -288,8 +288,8 @@
     1.4  
     1.5  fun proof_local cmd goal_ctxt int after_qed' propss =
     1.6    Proof.map_context (K goal_ctxt) #>
     1.7 -  Proof.local_goal (Proof_Display.print_results Isabelle_Markup.state int) (K I)
     1.8 -    Proof_Context.bind_propp_i cmd NONE after_qed' (map (pair Thm.empty_binding) propss);
     1.9 +  Proof.local_goal (K (K ())) (K I) Proof_Context.bind_propp_i cmd NONE
    1.10 +    after_qed' (map (pair Thm.empty_binding) propss);
    1.11  
    1.12  in
    1.13  

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