src/HOL/Tools/TFL/casesplit.ML
changeset 32091 30e2ffbba718
parent 32035 8e77b6a250d5
child 32712 ec5976f4d3d8
--- a/src/HOL/Tools/TFL/casesplit.ML	Tue Jul 21 00:56:19 2009 +0200
+++ b/src/HOL/Tools/TFL/casesplit.ML	Tue Jul 21 01:03:18 2009 +0200
@@ -269,9 +269,9 @@
       fun split th =
           (case find_thms_split splitths 1 th of
              NONE =>
-             (writeln "th:";
-              Display.print_thm th; writeln "split ths:";
-              Display.print_thms splitths; writeln "\n--";
+             (writeln (cat_lines
+              (["th:", Display.string_of_thm_without_context th, "split ths:"] @
+                map Display.string_of_thm_without_context splitths @ ["\n--"]));
               error "splitto: cannot find variable to split on")
             | SOME v =>
              let