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