ProgTutorial/Solutions.thy
changeset 440 a0b280dd4bc7
parent 426 d94755882e36
child 441 520127b708e6
--- 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