# HG changeset patch
# User wenzelm
# Date 1320359551 -3600
# Node ID dd8208a3655a95e716411f913a2b24ca8735cd05
# Parent  e5b33eecbf6e8d5732b360913d611a6ad6d7da88
tuned whitespace;

diff -r e5b33eecbf6e -r dd8208a3655a src/Pure/Isar/element.ML
--- 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