diff -r ce43c04d227d -r d94755882e36 ProgTutorial/Helper/Command/Command.thy
--- a/ProgTutorial/Helper/Command/Command.thy	Mon May 24 20:02:11 2010 +0100
+++ b/ProgTutorial/Helper/Command/Command.thy	Thu May 27 10:39:07 2010 +0200
@@ -5,9 +5,9 @@
 ML {*
 let
    val do_nothing = Scan.succeed (Local_Theory.theory I)
-   val kind = OuterKeyword.thy_decl
+   val kind = Keyword.thy_decl
 in
-   OuterSyntax.local_theory "foobar" "description of foobar" kind do_nothing
+   Outer_Syntax.local_theory "foobar" "description of foobar" kind do_nothing
 end
 *}
 
@@ -15,10 +15,10 @@
 let
   fun trace_prop str =
      Local_Theory.theory (fn lthy => (tracing str; lthy))
-  val trace_prop_parser = OuterParse.prop >> trace_prop
-  val kind = OuterKeyword.thy_decl
+  val trace_prop_parser = Parse.prop >> trace_prop
+  val kind = Keyword.thy_decl
 in
-  OuterSyntax.local_theory "foobar_trace" "traces a proposition"
+  Outer_Syntax.local_theory "foobar_trace" "traces a proposition"
     kind trace_prop_parser
 end
 *}
@@ -31,10 +31,10 @@
      in
        Proof.theorem NONE (K I) [[(prop,[])]] lthy
      end;
-   val prove_prop_parser = OuterParse.prop >> prove_prop
-   val kind = OuterKeyword.thy_goal
+   val prove_prop_parser = Parse.prop >> prove_prop
+   val kind = Keyword.thy_goal
 in
-   OuterSyntax.local_theory_to_proof "foobar_goal" "proving a proposition"
+   Outer_Syntax.local_theory_to_proof "foobar_goal" "proving a proposition"
      kind prove_prop_parser
 end
 *}
@@ -54,22 +54,13 @@
      Proof.theorem NONE (after_qed thm_name) [[(trm,[])]] lthy
    end
 
-   val parser = SpecParse.opt_thm_name ":" -- OuterParse.ML_source
+   val parser = Parse_Spec.opt_thm_name ":" -- Parse.ML_source
  
 in
-   OuterSyntax.local_theory_to_proof "foobar_prove" "proving a proposition" 
-     OuterKeyword.thy_goal (parser >> setup_proof)
+   Outer_Syntax.local_theory_to_proof "foobar_prove" "proving a proposition" 
+     Keyword.thy_goal (parser >> setup_proof)
 end*}
 
 
-(*
-ML {*
-let
-   val do_nothing = Scan.succeed (Local_Theory.theory I)
-   val kind = OuterKeyword.thy_decl
-in
-   OuterSyntax.local_theory "simple_inductive" "description of foobar" kind do_nothing
-end
-*}*)
 
 end