src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML
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,