--- a/src/Pure/Isar/element.ML Tue Feb 28 14:24:37 2012 +0100
+++ b/src/Pure/Isar/element.ML Tue Feb 28 16:43:32 2012 +0100
@@ -287,8 +287,8 @@
fun proof_local cmd goal_ctxt int after_qed' propss =
Proof.map_context (K goal_ctxt) #>
- Proof.local_goal (Proof_Display.print_results int) (K I) Proof_Context.bind_propp_i
- cmd NONE after_qed' (map (pair Thm.empty_binding) propss);
+ 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);
in