--- a/ProgTutorial/Parsing.thy	Mon Sep 28 01:21:27 2009 +0200
+++ b/ProgTutorial/Parsing.thy	Mon Sep 28 23:52:06 2009 +0200
@@ -1070,22 +1070,24 @@
 
 ML_val{*val r = ref (NONE:(unit -> term) option)*}
 ML{*let
-   fun setup_proof (txt, pos) lthy =
+   fun after_qed thm_name thms lthy =
+        LocalTheory.note Thm.theoremK (thm_name, (flat thms)) lthy |> snd
+
+   fun setup_proof (thm_name, (txt, pos)) lthy =
    let
      val trm = ML_Context.evaluate lthy true ("r", r) txt
    in
-       Proof.theorem_i NONE (K I) [[(trm,[])]] lthy
-   end;
+     Proof.theorem_i NONE (after_qed thm_name) [[(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 "foobar_prove" "proving a proposition" 
-    kind setup_proof_parser
+     OuterKeyword.thy_goal (parser >> setup_proof)
 end*}
 
-foobar_prove {* @{prop "True"} *}
+foobar_prove test: {* @{prop "True"} *}
 apply(rule TrueI)
 done