# HG changeset patch
# User blanchet
# Date 1285951717 -7200
# Node ID 44cd24da1beb4138f14afd170dfa0f3d59b60e94
# Parent  b0be1daf0667d6582dd696a0c9abd1bf890fadf2
tune whitespace

diff -r b0be1daf0667 -r 44cd24da1beb src/HOL/Tools/Sledgehammer/meson_clausify.ML
--- a/src/HOL/Tools/Sledgehammer/meson_clausify.ML	Fri Oct 01 17:56:32 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/meson_clausify.ML	Fri Oct 01 18:48:37 2010 +0200
@@ -340,7 +340,7 @@
               |>> the_single |>> cterm_of thy
           in (SOME (discharger_th, ct), Thm.assume ct, ctxt) end
        else
-          (NONE, th, ctxt)
+         (NONE, th, ctxt)
       end
     else
       (NONE, th, ctxt)