--- 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));