changeset 38433 | 1e28e2e1c2fb |
parent 38280 | 577f138af235 |
child 38549 | d0385f2764d8 |
child 38606 | 3003ddbd46d9 |
--- a/src/HOL/Tools/Sledgehammer/metis_tactics.ML Sun Aug 15 17:14:10 2010 +0200 +++ b/src/HOL/Tools/Sledgehammer/metis_tactics.ML Mon Aug 16 09:39:05 2010 +0200 @@ -789,7 +789,7 @@ Meson.MESON (maps neg_clausify) (fn cls => resolve_tac (FOL_SOLVE mode ctxt cls ths) 1) ctxt i st0 - handle ERROR msg => raise METIS ("generic_metis_tac", msg) + handle ERROR msg => raise METIS ("generic_metis_tac", msg) end handle METIS (loc, msg) => if mode = HO then