1.1 --- a/src/HOL/Tools/Sledgehammer/metis_tactics.ML	Wed Jun 02 11:53:17 2010 +0200
     1.2 +++ b/src/HOL/Tools/Sledgehammer/metis_tactics.ML	Wed Jun 02 12:28:42 2010 +0200
     1.3 @@ -409,9 +409,10 @@
     1.4            (substs' |> map (fn (x, y) =>
     1.5              Syntax.string_of_term ctxt (term_of x) ^ " |-> " ^
     1.6              Syntax.string_of_term ctxt (term_of y)))));
     1.7 -  in  cterm_instantiate substs' i_th
     1.8 -      handle THM (msg, _, _) => error ("metis error (inst_inf): " ^ msg)
     1.9 -  end;
    1.10 +  in  cterm_instantiate substs' i_th end
    1.11 +  handle THM (msg, _, _) => error ("metis error (inst_inf):\n" ^ msg)
    1.12 +       | ERROR msg => error ("metis error (inst_inf):\n" ^ msg ^
    1.13 +                             "\n(Perhaps you want to try \"metisFT\".)")
    1.14  
    1.15  (* INFERENCE RULE: RESOLVE *)
    1.16