# HG changeset patch
# User steckerm
# Date 1411202664 -7200
# Node ID bd5e49fca1fdb18c743fd465207a51d2a9aa6794
# Parent  111d801b5d5d795274c05f2d3eb225bc16505814
Removed double space

diff -r 111d801b5d5d -r bd5e49fca1fd src/HOL/Tools/ATP/atp_waldmeister.ML
--- a/src/HOL/Tools/ATP/atp_waldmeister.ML	Sat Sep 20 10:44:24 2014 +0200
+++ b/src/HOL/Tools/ATP/atp_waldmeister.ML	Sat Sep 20 10:44:24 2014 +0200
@@ -545,7 +545,7 @@
   NONE => NONE
 
 fun fix_name name = 
-  if  String.isPrefix fact_prefix name andalso String.isSuffix "_J" name then
+  if String.isPrefix fact_prefix name andalso String.isSuffix "_J" name then
     String.extract(name, size fact_prefix + 2,NONE) |> unascii_of |> 
     (fn x => fact_prefix ^ "0_" ^ x)
   else