# HG changeset patch
# User haftmann
# Date 1294059702 -3600
# Node ID 9acb7c5015307f7d4fcc3b108e1fc65933bf968c
# Parent  7ee22760436ccbd4b000c6ddda615ccd88705b78
tuned whitespace

diff -r 7ee22760436c -r 9acb7c501530 src/Pure/Isar/element.ML
--- a/src/Pure/Isar/element.ML	Fri Dec 31 00:11:24 2010 +0100
+++ b/src/Pure/Isar/element.ML	Mon Jan 03 14:01:42 2011 +0100
@@ -289,6 +289,7 @@
     Proof.map_context (K goal_ctxt)
     #> Proof.local_goal (Proof_Display.print_results int) (K I) ProofContext.bind_propp_i
       cmd NONE after_qed' (map (pair Thm.empty_binding) propss);
+
 in
 
 fun witness_proof after_qed wit_propss =
@@ -303,6 +304,7 @@
 
 fun witness_local_proof_eqs after_qed cmd wit_propss eq_props goal_ctxt int =
   gen_witness_proof (proof_local cmd goal_ctxt int) after_qed wit_propss eq_props;
+
 end;