# HG changeset patch # User blanchet # Date 1283427923 -7200 # Node ID dfea12cc5f5a74dd6319bce11d5f34ab06570fed # Parent 5146d640aa4af4f3389d93b0e5dcf245cf73481a FIXME -> TODO (nothing is broken) diff -r 5146d640aa4a -r dfea12cc5f5a src/HOL/Tools/Sledgehammer/metis_tactics.ML --- a/src/HOL/Tools/Sledgehammer/metis_tactics.ML Thu Sep 02 13:18:19 2010 +0200 +++ b/src/HOL/Tools/Sledgehammer/metis_tactics.ML Thu Sep 02 13:45:23 2010 +0200 @@ -802,7 +802,7 @@ if exists_type type_has_top_sort (prop_of st0) then (warning ("Metis: Proof state contains the universal sort {}"); Seq.empty) else - Meson.MESON (K all_tac) (* FIXME: Try (cnf.cnfx_rewrite_tac ctxt) *) + Meson.MESON (K all_tac) (* TODO: Try (cnf.cnfx_rewrite_tac ctxt) *) (maps neg_clausify) (fn cls => resolve_tac (FOL_SOLVE mode ctxt cls ths) 1) ctxt i st0