diff -r c0cae24b9d46 -r 5dffcab68680 ProgTutorial/Solutions.thy --- a/ProgTutorial/Solutions.thy Sat Oct 03 13:01:39 2009 +0200 +++ b/ProgTutorial/Solutions.thy Sat Oct 03 19:10:23 2009 +0200 @@ -1,5 +1,5 @@ theory Solutions -imports Base "Recipes/Timing" +imports FirstSteps "Recipes/Timing" begin chapter {* Solutions to Most Exercises\label{ch:solutions} *} @@ -288,7 +288,7 @@ This function generates for example: @{ML_response_fake [display,gray] - "writeln (Syntax.string_of_term @{context} (term_tree 2))" + "writeln (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