ProgTutorial/Solutions.thy
changeset 329 5dffcab68680
parent 328 c0cae24b9d46
child 346 0fea8b7a14a1
--- 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