--- a/ProgTutorial/Helper/Command/Command.thy	Sun Dec 15 23:49:05 2013 +0000
+++ b/ProgTutorial/Helper/Command/Command.thy	Thu Mar 13 17:16:49 2014 +0000
@@ -7,7 +7,6 @@
 ML {*
 let
    val do_nothing = Scan.succeed (Local_Theory.background_theory I)
-   val kind = Keyword.thy_decl
 in
    Outer_Syntax.local_theory @{command_spec "foobar"} 
      "description of foobar" 
@@ -20,7 +19,6 @@
   fun trace_prop str =
      Local_Theory.background_theory (fn lthy => (tracing str; lthy))
   val trace_prop_parser = Parse.prop >> trace_prop
-  val kind = Keyword.thy_decl
 in
   Outer_Syntax.local_theory @{command_spec "foobar_trace"} 
     "traces a proposition"
@@ -37,7 +35,6 @@
        Proof.theorem NONE (K I) [[(prop,[])]] lthy
      end;
    val prove_prop_parser = Parse.prop >> prove_prop
-   val kind = Keyword.thy_goal
 in
    Outer_Syntax.local_theory_to_proof @{command_spec "foobar_goal"} 
      "proving a proposition"
@@ -58,9 +55,9 @@
    fun after_qed thm_name thms lthy =
         Local_Theory.note (thm_name, (flat thms)) lthy |> snd
 
-   fun setup_proof (thm_name, (txt, pos)) lthy =
+   fun setup_proof (thm_name, {text, ...}) lthy =
    let
-     val trm = Code_Runtime.value lthy result_cookie ("", txt)
+     val trm = Code_Runtime.value lthy result_cookie ("", text)
    in
      Proof.theorem NONE (after_qed thm_name) [[(trm,[])]] lthy
    end