
diff -r 29787dcf7b2e -r b63c72776f03 ProgTutorial/Solutions.thy
--- a/ProgTutorial/Solutions.thy	Mon Apr 13 08:30:48 2009 +0000
+++ b/ProgTutorial/Solutions.thy	Wed Apr 15 13:11:08 2009 +0000
@@ -170,7 +170,7 @@
   This function generates for example:
 
   @{ML_response_fake [display,gray] 
-  "warning (Syntax.string_of_term @{context} (term_tree 2))" 
+  "writeln (Syntax.string_of_term @{context} (term_tree 2))" 
   "(1 + 2) + (3 + 4)"} 
 
   The next function constructs a goal of the form @{text "P \<dots>"} with a term 




