--- a/ProgTutorial/Tactical.thy	Sat Oct 03 13:01:39 2009 +0200
+++ b/ProgTutorial/Tactical.thy	Sat Oct 03 19:10:23 2009 +0200
@@ -1655,7 +1655,7 @@
 ML{*fun fail_simproc' simpset redex = 
 let
   val ctxt = Simplifier.the_context simpset
-  val _ = tracing ("The redex: " ^ (Syntax.string_of_term ctxt redex))
+  val _ = tracing ("The redex: " ^ (string_of_term ctxt redex))
 in
   NONE
 end*}