inlined nospaces (from library.ML);

--- a/src/HOL/Tools/ATP/AtpCommunication.ML	Thu Dec 28 10:04:10 2006 +0100
+++ b/src/HOL/Tools/ATP/AtpCommunication.ML	Thu Dec 28 14:30:38 2006 +0100
@@ -60,6 +60,9 @@
     
 fun not_comma c = c <>  #",";
 
+val nospaces = String.translate (fn c => if Char.isSpace c then "" else str c);
+
+
 (*A valid TSTP axiom line has the form  cnf(NNN,axiom,...) where NNN is a positive integer.*)
 fun parse_tstp_line s =
   let val ss = Substring.full (unprefix "cnf(" (nospaces s))