--- a/ProgTutorial/Base.thy	Tue Jul 14 01:42:35 2009 +0200
+++ b/ProgTutorial/Base.thy	Tue Jul 14 16:34:24 2009 +0200
@@ -1,5 +1,5 @@
 theory Base
-imports Main
+imports Main LaTeXsugar
 uses
   "output_tutorial.ML"
   "chunks.ML"
@@ -11,17 +11,17 @@
 
 fun propagate_env (context as Context.Proof lthy) =
       Context.Proof (LocalTheory.map_contexts (ML_Env.inherit context) lthy)
-  | propagate_env context = context;
+  | propagate_env context = context
 
 fun propagate_env_prf prf = Proof.map_contexts
-  (Context.proof_map (ML_Env.inherit (Context.Proof (Proof.context_of prf)))) prf;
+  (Context.proof_map (ML_Env.inherit (Context.Proof (Proof.context_of prf)))) prf
 
 val _ =
   OuterSyntax.command "ML" "eval ML text within theory"
     (OuterKeyword.tag "TutorialML" OuterKeyword.thy_decl)
     (OuterParse.ML_source >> (fn (txt, pos) =>
       Toplevel.generic_theory
-        (ML_Context.exec (fn () => ML_Context.eval true pos txt) #> propagate_env)));
+        (ML_Context.exec (fn () => ML_Context.eval true pos txt) #> propagate_env)))
 
 val _ =
   OuterSyntax.command "ML_prf" "ML text within proof" 
@@ -33,7 +33,7 @@
 val _ =
   OuterSyntax.command "ML_val" "diagnostic ML text" 
   (OuterKeyword.tag "TutorialML" OuterKeyword.diag)
-    (OuterParse.ML_source >> IsarCmd.ml_diag true);
+    (OuterParse.ML_source >> IsarCmd.ml_diag true)
 
 *}