diff -r 29787dcf7b2e -r b63c72776f03 ProgTutorial/FirstSteps.thy
--- a/ProgTutorial/FirstSteps.thy	Mon Apr 13 08:30:48 2009 +0000
+++ b/ProgTutorial/FirstSteps.thy	Wed Apr 15 13:11:08 2009 +0000
@@ -95,21 +95,21 @@
 
   During development you might find it necessary to inspect some data
   in your code. This can be done in a ``quick-and-dirty'' fashion using 
-  the function @{ML "warning"}. For example 
+  the function @{ML "writeln"}. For example 
 
-  @{ML_response_fake [display,gray] "warning \"any string\"" "\"any string\""}
+  @{ML_response_fake [display,gray] "writeln \"any string\"" "\"any string\""}
 
   will print out @{text [quotes] "any string"} inside the response buffer
   of Isabelle.  This function expects a string as argument. If you develop under PolyML,
   then there is a convenient, though again ``quick-and-dirty'', method for
   converting values into strings, namely the function @{ML makestring}:
 
-  @{ML_response_fake [display,gray] "warning (makestring 1)" "\"1\""} 
+  @{ML_response_fake [display,gray] "writeln (makestring 1)" "\"1\""} 
 
   However, @{ML makestring} only works if the type of what is converted is monomorphic 
   and not a function.
 
-  The function @{ML "warning"} should only be used for testing purposes, because any
+  The function @{ML "writeln"} should only be used for testing purposes, because any
   output this function generates will be overwritten as soon as an error is
   raised. For printing anything more serious and elaborate, the
   function @{ML tracing} is more appropriate. This function writes all output into
@@ -173,10 +173,10 @@
   "\"\\^E\\^Fterm\\^E\\^E\\^Fconst\\^Fname=HOL.one_class.one\\^E1\\^E\\^F\\^E\\^E\\^F\\^E\""}
 
   This produces a string with some additional information encoded in it. The string
-  can be properly printed by using the function @{ML warning}.
+  can be properly printed by using the function @{ML writeln}.
 
   @{ML_response_fake [display,gray]
-  "warning (Syntax.string_of_term @{context} @{term \"1::nat\"})"
+  "writeln (Syntax.string_of_term @{context} @{term \"1::nat\"})"
   "\"1\""}
 
   A @{ML_type cterm} can be transformed into a string by the following function.
@@ -207,7 +207,7 @@
   @{text "?Q"} and so on. 
 
   @{ML_response_fake [display, gray]
-  "warning (str_of_thm @{context} @{thm conjI})"
+  "writeln (str_of_thm @{context} @{thm conjI})"
   "\<lbrakk>?P; ?Q\<rbrakk> \<Longrightarrow> ?P \<and> ?Q"}
 
   In order to improve the readability of theorems we convert
@@ -229,7 +229,7 @@
   Theorem @{thm [source] conjI} is now printed as follows:
 
   @{ML_response_fake [display, gray]
-  "warning (str_of_thm_no_vars @{context} @{thm conjI})"
+  "writeln (str_of_thm_no_vars @{context} @{thm conjI})"
   "\<lbrakk>P; Q\<rbrakk> \<Longrightarrow> P \<and> Q"}
   
   Again the function @{ML commas} helps with printing more than one theorem. 
@@ -333,7 +333,7 @@
   @{ML_response_fake [display,gray]
 "apply_fresh_args @{term \"P::nat \<Rightarrow> int \<Rightarrow> unit \<Rightarrow> bool\"} @{context} 
  |> Syntax.string_of_term @{context}
- |> warning"
+ |> writeln"
   "P z za zb"}
 
   You can read off this behaviour from how @{ML apply_fresh_args} is
@@ -1629,7 +1629,7 @@
          case realOut (!r) of
             NONE => "NONE"
           | SOME x => Real.toString x
-      val () = warning (concat [s1, " ", s2, " ", s3, "\n"])
+      val () = writeln (concat [s1, " ", s2, " ", s3, "\n"])
    end*}
 
 ML_val{*structure t = Test(U) *}