diff -r 68a770a8a09f -r ddf6deaadfe8 src/HOL/Tools/Metis/metis_tactic.ML
--- a/src/HOL/Tools/Metis/metis_tactic.ML	Wed Mar 04 20:50:20 2015 +0100
+++ b/src/HOL/Tools/Metis/metis_tactic.ML	Wed Mar 04 22:05:01 2015 +0100
@@ -49,7 +49,7 @@
       Const (@{const_name HOL.eq}, _) $ _ $ t =>
       let
         val ct = Thm.cterm_of thy t
-        val cT = Thm.ctyp_of_term ct
+        val cT = Thm.ctyp_of_cterm ct
       in refl |> Drule.instantiate' [SOME cT] [SOME ct] end
     | Const (@{const_name disj}, _) $ t1 $ t2 =>
       (if can HOLogic.dest_not t1 then t2 else t1)