--- a/Prove.thy	Mon Sep 28 19:15:19 2009 +0200
+++ b/Prove.thy	Mon Sep 28 19:22:28 2009 +0200
@@ -5,6 +5,7 @@
 ML {*
 val r = ref (NONE:(unit -> term) option)
 *}
+
 ML {*
 let
    fun setup_proof (txt, pos) lthy =
@@ -18,9 +19,11 @@
         
    val kind = OuterKeyword.thy_goal
 in
-   OuterSyntax.local_theory_to_proof "prove" "proving a proposition" 
+  OuterSyntax.local_theory_to_proof "prove" "proving a proposition" 
     kind setup_proof_parser
 end
 *}
 
+
+
 end