# HG changeset patch
# User wenzelm
# Date 1457386604 -3600
# Node ID 53603d1aad5fb25c37f8ea6b37bc61f370740bfd
# Parent  df62e1ab7d884eb2a7ff0033200673674ef09ea2
proper Path.print for user messages;

diff -r df62e1ab7d88 -r 53603d1aad5f src/HOL/TPTP/TPTP_Parser/tptp_interpret.ML
--- a/src/HOL/TPTP/TPTP_Parser/tptp_interpret.ML	Mon Mar 07 21:53:21 2016 +0100
+++ b/src/HOL/TPTP/TPTP_Parser/tptp_interpret.ML	Mon Mar 07 22:36:44 2016 +0100
@@ -756,8 +756,7 @@
   case find_first (fn prefix => File.exists (Path.append prefix path_suffix))
          path_prefixes of
     SOME prefix => Path.append prefix path_suffix
-  | NONE =>
-    error ("Cannot find include file " ^ quote (Path.implode path_suffix))
+  | NONE => error ("Cannot find include file " ^ Path.print path_suffix)
 
 (* Ideally, to be in sync with TFF1, we should perform full type skolemization here.
    But the problems originating from HOL systems are restricted to top-level
diff -r df62e1ab7d88 -r 53603d1aad5f src/HOL/TPTP/TPTP_Parser/tptp_reconstruct.ML
--- a/src/HOL/TPTP/TPTP_Parser/tptp_reconstruct.ML	Mon Mar 07 21:53:21 2016 +0100
+++ b/src/HOL/TPTP/TPTP_Parser/tptp_reconstruct.ML	Mon Mar 07 22:36:44 2016 +0100
@@ -1797,7 +1797,7 @@
     val fms = get_fmlas_of_prob thy1 prob_name
   in
     if List.null fms then
-      (warning ("File " ^ Path.implode file_name ^ " appears empty!");
+      (warning ("File " ^ Path.print file_name ^ " appears empty!");
        TPTP_Reconstruction_Data.map (cons ((prob_name, empty_pannot prob_name))) thy1)
     else
       let