--- a/src/Pure/Isar/element.ML Thu Nov 03 22:51:37 2011 +0100
+++ b/src/Pure/Isar/element.ML Thu Nov 03 23:32:31 2011 +0100
@@ -294,9 +294,9 @@
in proof after_qed' propss #> refine_witness #> Seq.hd end;
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.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);
in