--- a/Prove.thy	Mon Sep 28 19:24:55 2009 +0200
+++ b/Prove.thy	Mon Sep 28 23:17:29 2009 +0200
@@ -8,19 +8,21 @@
 
 ML {*
 let
-   fun setup_proof (txt, pos) lthy =
-   let
-     val trm = ML_Context.evaluate lthy true ("r", r) txt
-   in
-       Proof.theorem_i NONE (K I) [[(trm,[])]] lthy
-   end;
+  fun after_qed thm_name thms lthy =
+       LocalTheory.note Thm.theoremK (thm_name, (flat thms)) lthy |> snd
+    
+  fun setup_proof (name_spec, (txt, pos)) lthy =
+  let
+    val trm = ML_Context.evaluate lthy true ("r", r) txt
+  in
+    Proof.theorem_i NONE (after_qed name_spec) [[(trm,[])]] lthy
+  end;
 
-   val setup_proof_parser = OuterParse.ML_source >> setup_proof
-        
-   val kind = OuterKeyword.thy_goal
+  val parser = SpecParse.opt_thm_name ":" -- OuterParse.ML_source
+
 in
   OuterSyntax.local_theory_to_proof "prove" "proving a proposition" 
-    kind setup_proof_parser
+    OuterKeyword.thy_goal (parser >> setup_proof)
 end
 *}