src/HOL/Tools/TFL/casesplit.ML

           Thm.biresolution false [(false,split)] 1 th;
 
       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
                val gt = Data.dest_Trueprop (List.nth(Thm.prems_of th, 0));
                val split_thm = mk_casesplit_goal_thm sgn v gt;