# HG changeset patch
# User wenzelm
# Date 869586342 -7200
# Node ID de164676a2023620f85e7ee4df1c60035d8719b8
# Parent  4336eb0486bc417de6a3af79c7f2d55bdba0a61d
improved print_cs;

diff -r 4336eb0486bc -r de164676a202 src/Provers/classical.ML
--- a/src/Provers/classical.ML	Tue Jul 22 11:49:59 1997 +0200
+++ b/src/Provers/classical.ML	Tue Jul 22 17:45:42 1997 +0200
@@ -196,12 +196,13 @@
      haz_netpair   = (Net.empty,Net.empty),
      dup_netpair   = (Net.empty,Net.empty)};
 
-fun print_cs (CS{safeIs,safeEs,hazIs,hazEs,...}) =
- (writeln"Introduction rules";  	prths hazIs;
-  writeln"Safe introduction rules";  	prths safeIs;
-  writeln"Elimination rules";  		prths hazEs;
-  writeln"Safe elimination rules";  	prths safeEs;
-  ());
+fun print_cs (CS {safeIs, safeEs, hazIs, hazEs, ...}) =
+  let val pretty_thms = map Display.pretty_thm in
+    Pretty.writeln (Pretty.big_list "introduction rules:" (pretty_thms hazIs));
+    Pretty.writeln (Pretty.big_list "safe introduction rules:" (pretty_thms safeIs));
+    Pretty.writeln (Pretty.big_list "elimination rules:" (pretty_thms hazEs));
+    Pretty.writeln (Pretty.big_list "safe elimination rules:" (pretty_thms safeEs))
+  end;
 
 fun rep_claset (CS args) = args;