diff -r a0b280dd4bc7 -r 520127b708e6 ProgTutorial/Package/Ind_Code.thy
--- a/ProgTutorial/Package/Ind_Code.thy	Tue Jul 20 13:34:44 2010 +0100
+++ b/ProgTutorial/Package/Ind_Code.thy	Wed Jul 28 19:09:49 2010 +0200
@@ -1,5 +1,5 @@
 theory Ind_Code
-imports Ind_General_Scheme "../FirstSteps" 
+imports Ind_General_Scheme "../First_Steps" 
 begin
 
 section {* The Gory Details\label{sec:code} *} 
@@ -92,7 +92,7 @@
 let
   val def = defn_aux lthy eo_orules eo_preds (e_pred, e_arg_tys)
 in
-  tracing (string_of_term lthy def); lthy
+  pwriteln (pretty_term lthy def); lthy
 end *}
 
 text {*
@@ -112,7 +112,7 @@
   val arg = (fresh_pred, fresh_arg_tys)
   val def = defn_aux lthy fresh_orules [fresh_pred] arg
 in
-  tracing (string_of_term lthy def); lthy
+  pwriteln (pretty_term lthy def); lthy
 end *}
 
 
@@ -596,7 +596,7 @@
             Pretty.big_list "Prems2 from the predicate:" (map (pretty_thm ctxt) prems2)] 
 in 
   pps |> Pretty.chunks
-      |> tracing o Pretty.string_of
+      |> pwriteln
 end*}
 text_raw{*
 \end{isabelle}