# HG changeset patch
# User berghofe
# Date 1098218720 -7200
# Node ID d4f1b11c336b1862bab2de04620442f738c31e7d
# Parent  bb6f072c8d10fe3376b6efc86cfc607a43a004bd
Replaced PolyML specific print function by Display.print_thm(s)

diff -r bb6f072c8d10 -r d4f1b11c336b TFL/casesplit.ML
--- a/TFL/casesplit.ML	Tue Oct 19 18:18:45 2004 +0200
+++ b/TFL/casesplit.ML	Tue Oct 19 22:45:20 2004 +0200
@@ -306,9 +306,9 @@
           (case find_thms_split splitths 1 th of 
              None => 
              (writeln "th:";
-              print th; writeln "split ths:";
-             print splitths; writeln "\n--";
-             raise ERROR_MESSAGE "splitto: cannot find variable to split on")
+              Display.print_thm th; writeln "split ths:";
+              Display.print_thms splitths; writeln "\n--";
+              raise ERROR_MESSAGE "splitto: cannot find variable to split on")
             | Some v => 
              let 
                val gt = Data.dest_Trueprop (nth_elem(0, Thm.prems_of th));