--- a/Prove.thy	Tue Sep 29 17:46:18 2009 +0200
+++ b/Prove.thy	Tue Sep 29 22:35:48 2009 +0200
@@ -16,16 +16,13 @@
     val trm = ML_Context.evaluate lthy true ("r", r) txt
   in
     Proof.theorem_i NONE (after_qed name_spec) [[(trm,[])]] lthy
-  end;
+  end
 
   val parser = SpecParse.opt_thm_name ":" -- OuterParse.ML_source
-
 in
   OuterSyntax.local_theory_to_proof "prove" "proving a proposition" 
     OuterKeyword.thy_goal (parser >> setup_proof)
 end
 *}
 
-
-
 end