diff -r 6eeee59dac4c -r 014090d1e64b src/HOL/Tools/ATP/recon_transfer_proof.ML
--- a/src/HOL/Tools/ATP/recon_transfer_proof.ML	Wed Jul 13 16:07:23 2005 +0200
+++ b/src/HOL/Tools/ATP/recon_transfer_proof.ML	Wed Jul 13 16:07:24 2005 +0200
@@ -9,11 +9,11 @@
 
 structure Recon_Transfer =
 struct
+
 open Recon_Parse
+
 infixr 8 ++; infixr 7 >>; infixr 6 ||;
 
-fun not_newline ch = not (ch = "\n");
-
 
 
 (*
@@ -51,14 +51,9 @@
 
 (* Versions that include type information *)
  
+(* FIXME rename to str_of_thm *)
 fun string_of_thm thm =
-  let val _ = set show_sorts
-      val str = Display.string_of_thm thm
-      val no_returns =List.filter not_newline (explode str)
-      val _ = reset show_sorts
-  in 
-      implode no_returns
-  end
+  setmp show_sorts true (Pretty.str_of o Display.pretty_thm) thm;
 
 
 (* check separate args in the watcher program for separating strings with a * or ; or something *)
@@ -377,31 +372,16 @@
 \1453[0:Rew:1279.0,1430.0,1242.0,1430.0,1279.0,1430.0] || equal(const_0,const_0)* -> .\
 \1454[0:Obv:1453.0] ||  -> .";*)
 
-fun remove_linebreaks str = let val strlist = explode str
-	                        val nonewlines = filter (not_equal "\n") strlist
-	                    in
-				implode nonewlines
-			    end
-
+fun subst_for a b [] = ""
+  | subst_for a b (x :: xs) =
+      if x = a
+      then 
+	b ^ subst_for a b xs
+      else
+	x ^ subst_for a b xs;
 
-fun subst_for a b [] = ""
-|   subst_for a b (x::xs) = if (x = a)
-				   then 
-					(b^(subst_for a b  xs))
-				   else
-					x^(subst_for a b xs)
-
-
-fun remove_linebreaks str = let val strlist = explode str
-			    in
-				subst_for "\n" "\t" strlist
-			    end
-
-fun restore_linebreaks str = let val strlist = explode str
-			     in
-				subst_for "\t" "\n" strlist
-			     end
-
+val remove_linebreaks = subst_for "\n" "\t" o explode;
+val restore_linebreaks = subst_for "\t" "\n" o explode;
 
 
 fun spassString_to_lemmaString proofstr thmstring goalstring toParent ppid thms clause_arr  num_of_clauses  =