--- a/ProgTutorial/Helper/Command/Command.thy	Mon Sep 28 01:21:27 2009 +0200
+++ b/ProgTutorial/Helper/Command/Command.thy	Mon Sep 28 23:52:06 2009 +0200
@@ -42,23 +42,25 @@
 ML {*
 val r = ref (NONE:(unit -> term) option)
 *}
-ML {*
+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
-end
-*}
+     OuterKeyword.thy_goal (parser >> setup_proof)
+end*}
+
 
 (*
 ML {*