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