--- a/ProgTutorial/Package/Ind_Code.thy	Fri Aug 13 18:52:16 2010 +0800
+++ b/ProgTutorial/Package/Ind_Code.thy	Sun Aug 22 22:56:52 2010 +0800
@@ -596,8 +596,10 @@
             Pretty.big_list "Prems2 from the predicate:" (map (pretty_thm ctxt) prems2)] 
 in 
   pps |> Pretty.chunks
-      |> pwriteln
+      |> Pretty.string_of
+      |> tracing
 end*}
+
 text_raw{*
 \end{isabelle}
 \end{minipage}
@@ -788,6 +790,7 @@
   of the accessible part is such a rule. 
 *}
 
+
 lemma accpartI:
 shows "\<And>R x. (\<And>y. R y x \<Longrightarrow> accpart R y) \<Longrightarrow> accpart R x"
 apply(tactic {* expand_tac @{thms accpart_def} *})