# HG changeset patch
# User wenzelm
# Date 1167312638 -3600
# Node ID 71e312d6d19a5ca12dfa2ad8f8be6a600cbb6931
# Parent  12b8fde1f9c019ea01ed563efb0c4e20041c9450
inlined nospaces (from library.ML);

diff -r 12b8fde1f9c0 -r 71e312d6d19a src/HOL/Tools/ATP/AtpCommunication.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))