# HG changeset patch
# User blanchet
# Date 1306485196 -7200
# Node ID b967219cec7836c6f405082e8973aa62363ac6a1
# Parent  07ebc23987319edd5596312417fa377286778cee
tuned comments

diff -r 07ebc2398731 -r b967219cec78 src/HOL/Tools/Sledgehammer/sledgehammer_atp_reconstruct.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_reconstruct.ML	Fri May 27 10:30:08 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_reconstruct.ML	Fri May 27 10:33:16 2011 +0200
@@ -85,11 +85,11 @@
                  | (_, value) => value) NONE vec
 
 
-(** SPASS's Flotter hack **)
+(** SPASS's FLOTTER hack **)
 
 (* This is a hack required for keeping track of facts after they have been
-   clausified by SPASS's Flotter tool. The "ATP/scripts/spass" script is also
-   part of this hack. *)
+   clausified by SPASS's FLOTTER preprocessor. The "ATP/scripts/spass" script is
+   also part of this hack. *)
 
 val set_ClauseFormulaRelationN = "set_ClauseFormulaRelation"
 
diff -r 07ebc2398731 -r b967219cec78 src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML	Fri May 27 10:30:08 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML	Fri May 27 10:33:16 2011 +0200
@@ -1249,7 +1249,7 @@
       |> (if should_add_ti_ti_helper type_sys then cons (ti_ti_helper_fact ())
           else I)
     (* Reordering these might confuse the proof reconstruction code or the SPASS
-       Flotter hack. *)
+       FLOTTER hack. *)
     val problem =
       [(explicit_declsN, sym_decl_lines),
        (factsN,