Replaced PolyML specific print function by Display.print_thm(s)
authorberghofe
Tue Oct 19 22:45:20 2004 +0200 (2004-10-19)
changeset 15252d4f1b11c336b
parent 15251 bb6f072c8d10
child 15253 6e20cc79bde6
Replaced PolyML specific print function by Display.print_thm(s)
TFL/casesplit.ML
     1.1 --- a/TFL/casesplit.ML	Tue Oct 19 18:18:45 2004 +0200
     1.2 +++ b/TFL/casesplit.ML	Tue Oct 19 22:45:20 2004 +0200
     1.3 @@ -306,9 +306,9 @@
     1.4            (case find_thms_split splitths 1 th of 
     1.5               None => 
     1.6               (writeln "th:";
     1.7 -              print th; writeln "split ths:";
     1.8 -             print splitths; writeln "\n--";
     1.9 -             raise ERROR_MESSAGE "splitto: cannot find variable to split on")
    1.10 +              Display.print_thm th; writeln "split ths:";
    1.11 +              Display.print_thms splitths; writeln "\n--";
    1.12 +              raise ERROR_MESSAGE "splitto: cannot find variable to split on")
    1.13              | Some v => 
    1.14               let 
    1.15                 val gt = Data.dest_Trueprop (nth_elem(0, Thm.prems_of th));