
diff -r b83c75d051b7 -r a0b280dd4bc7 ProgTutorial/Solutions.thy
--- a/ProgTutorial/Solutions.thy	Mon Jul 19 15:44:13 2010 +0100
+++ b/ProgTutorial/Solutions.thy	Tue Jul 20 13:34:44 2010 +0100
@@ -305,7 +305,7 @@
   This function generates for example:
 
   @{ML_response_fake [display,gray] 
-  "writeln (string_of_term @{context} (term_tree 2))" 
+  "pwriteln (pretty_term @{context} (term_tree 2))" 
   "(1 + 2) + (3 + 4)"} 
 
   The next function constructs a goal of the form @{text "P \<dots>"} with a term 




