diff -r 2e733b0a963c -r 6a7a9261b9ad src/HOL/Tools/Sledgehammer/metis_tactics.ML
--- a/src/HOL/Tools/Sledgehammer/metis_tactics.ML	Thu Jun 24 18:22:15 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/metis_tactics.ML	Thu Jun 24 21:00:37 2010 +0200
@@ -446,13 +446,15 @@
   of 1, and the use of RSN would increase this typically to 3. Instantiations of those Vars
   could then fail. See comment on mk_var.*)
 fun resolve_inc_tyvars(tha,i,thb) =
-  let val tha = Drule.incr_type_indexes (1 + Thm.maxidx_of thb) tha
+  let
+      val tha = Drule.incr_type_indexes (1 + Thm.maxidx_of thb) tha
       val ths = Seq.list_of (Thm.bicompose false (false,tha,nprems_of tha) i thb)
   in
       case distinct Thm.eq_thm ths of
         [th] => th
       | _ => raise THM ("resolve_inc_tyvars: unique result expected", i, [tha,thb])
-  end;
+  end
+  handle TERM (msg, _) => raise METIS ("resolve_inc_tyvars", msg)
 
 fun resolve_inf ctxt mode skolem_somes thpairs atm th1 th2 =
   let