changeset 43039 | b967219cec78 |
parent 43017 | 944b19ab6003 |
child 43064 | b6e61d22fa61 |
--- 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,