diff -r 8684b5240f11 -r ca87aff1ad2d src/FOLP/classical.ML
--- a/src/FOLP/classical.ML	Fri May 16 23:25:37 2008 +0200
+++ b/src/FOLP/classical.ML	Sat May 17 13:54:30 2008 +0200
@@ -124,10 +124,10 @@
 val empty_cs = make_cs{safeIs=[], safeEs=[], hazIs=[], hazEs=[]};
 
 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;
+ (writeln"Introduction rules";  Display.prths hazIs;
+  writeln"Safe introduction rules";  Display.prths safeIs;
+  writeln"Elimination rules";  Display.prths hazEs;
+  writeln"Safe elimination rules";  Display.prths safeEs;
   ());
 
 fun (CS{safeIs,safeEs,hazIs,hazEs,...}) addSIs ths =