--- a/ProgTutorial/Package/Ind_Code.thy	Sat Oct 03 13:01:39 2009 +0200
+++ b/ProgTutorial/Package/Ind_Code.thy	Sat Oct 03 19:10:23 2009 +0200
@@ -117,7 +117,7 @@
 let
   val def = defn_aux lthy eo_orules eo_preds (e_pred, e_arg_tys)
 in
-  tracing (Syntax.string_of_term lthy def); lthy
+  tracing (string_of_term lthy def); lthy
 end *}
 
 text {*
@@ -137,7 +137,7 @@
   val def = defn_aux lthy fresh_orules 
                              [fresh_pred] (fresh_pred, fresh_arg_tys)
 in
-  tracing (Syntax.string_of_term lthy def); lthy
+  tracing (string_of_term lthy def); lthy
 end *}