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 \"} with a term