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