--- 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"
--- 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,