# HG changeset patch
# User boehmes
# Date 1294071032 -3600
# Node ID 44511bf5dcc61edc719b9338b1a5884bdd8a0d1b
# Parent  5fbad03906491015dde40c83f3b441629372bc6d# Parent  9acb7c5015307f7d4fcc3b108e1fc65933bf968c
merged

diff -r 5fbad0390649 -r 44511bf5dcc6 src/Pure/Isar/element.ML
--- a/src/Pure/Isar/element.ML	Mon Jan 03 16:49:28 2011 +0100
+++ b/src/Pure/Isar/element.ML	Mon Jan 03 17:10:32 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;