--- a/ProgTutorial/Tactical.thy	Tue Jul 20 13:34:44 2010 +0100
+++ b/ProgTutorial/Tactical.thy	Wed Jul 28 19:09:49 2010 +0200
@@ -1,12 +1,12 @@
 theory Tactical
-imports Base FirstSteps
+imports Base First_Steps
 begin
 
 (*<*)
 setup{*
 open_file_with_prelude 
   "Tactical_Code.thy"
-  ["theory Tactical", "imports Base FirstSteps", "begin"]
+  ["theory Tactical", "imports Base First_Steps", "begin"]
 *}
 (*>*)
 
@@ -1831,7 +1831,7 @@
 ML %linenosgray{*fun fail_simproc simpset redex = 
 let
   val ctxt = Simplifier.the_context simpset
-  val _ = tracing ("The redex: " ^ (string_of_cterm ctxt redex))
+  val _ = pwriteln (Pretty.block [Pretty.str "The redex: ", pretty_cterm ctxt redex])
 in
   NONE
 end*}
@@ -1903,14 +1903,14 @@
 ML{*fun fail_simproc' simpset redex = 
 let
   val ctxt = Simplifier.the_context simpset
-  val _ = tracing ("The redex: " ^ (string_of_term ctxt redex))
+  val _ = pwriteln (Pretty.block [Pretty.str "The redex:", pretty_term ctxt redex])
 in
   NONE
 end*}
 
 text {*
   Here the redex is given as a @{ML_type term}, instead of a @{ML_type cterm}
-  (therefore we printing it out using the function @{ML string_of_term in Syntax}).
+  (therefore we printing it out using the function @{ML pretty_term in Pretty}).
   We can turn this function into a proper simproc using the function 
   @{ML Simplifier.simproc_i}:
 *}