--- a/ProgTutorial/Base.thy	Thu Jun 04 09:28:29 2009 +0200
+++ b/ProgTutorial/Base.thy	Fri Jun 05 04:17:28 2009 +0200
@@ -9,27 +9,26 @@
 (* to have a special tag for text enclosed in ML *)
 ML {*
 
-fun inherit_env (context as Context.Proof lthy) =
-      Context.Proof (LocalTheory.map_contexts (ML_Context.inherit_env context) lthy)
-  | inherit_env context = context;
+fun propagate_env (context as Context.Proof lthy) =
+      Context.Proof (LocalTheory.map_contexts (ML_Env.inherit context) lthy)
+  | propagate_env context = context;
 
-fun inherit_env_prf prf = Proof.map_contexts
-  (Context.proof_map (ML_Context.inherit_env (Context.Proof (Proof.context_of prf)))) prf
+fun propagate_env_prf prf = Proof.map_contexts
+  (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) #> inherit_env)));
-
+        (ML_Context.exec (fn () => ML_Context.eval true pos txt) #> propagate_env)));
 
 val _ =
   OuterSyntax.command "ML_prf" "ML text within proof" 
     (OuterKeyword.tag "TutorialML" OuterKeyword.prf_decl)
     (OuterParse.ML_source >> (fn (txt, pos) =>
       Toplevel.proof (Proof.map_context (Context.proof_map
-        (ML_Context.exec (fn () => ML_Context.eval true pos txt))) #> inherit_env_prf)))
+        (ML_Context.exec (fn () => ML_Context.eval true pos txt))) #> propagate_env_prf)))
 
 val _ =
   OuterSyntax.command "ML_val" "diagnostic ML text" 

--- a/ProgTutorial/FirstSteps.thy	Thu Jun 04 09:28:29 2009 +0200
+++ b/ProgTutorial/FirstSteps.thy	Fri Jun 05 04:17:28 2009 +0200
@@ -122,7 +122,7 @@
 
   @{ML_response_fake [display,gray] "writeln (PolyML.makestring 1)" "\"1\""} 
 
-  However, @{ML [index] makestring} only works if the type of what is converted is monomorphic 
+  However, @{ML [index] makestring in PolyML} only works if the type of what is converted is monomorphic 
   and not a function.
 
   The function @{ML "writeln"} should only be used for testing purposes, because any

Binary file progtutorial.pdf has changed