ProgTutorial/Package/Ind_Code.thy
changeset 305 2ac9dc1a95b4
parent 301 2728e8daebc0
child 315 de49d5780f57
--- a/ProgTutorial/Package/Ind_Code.thy	Wed Aug 05 08:58:28 2009 +0200
+++ b/ProgTutorial/Package/Ind_Code.thy	Wed Aug 05 09:24:18 2009 +0200
@@ -615,8 +615,7 @@
         @ ["Prems1 from the rule:"] @ (map (string_of_thm ctxt) prems1) 
         @ ["Prems2 from the predicate:"] @ (map (string_of_thm ctxt) prems2) 
 in 
-  s |> separate "\n"
-    |> implode
+  s |> cat_lines
     |> tracing
 end*}
 text_raw{*