diff -r eb59c6968219 -r b60e65ad13df src/HOL/Tools/Metis/metis_reconstruct.ML
--- a/src/HOL/Tools/Metis/metis_reconstruct.ML	Thu Mar 05 13:28:04 2015 +0100
+++ b/src/HOL/Tools/Metis/metis_reconstruct.ML	Fri Mar 06 00:00:57 2015 +0100
@@ -398,21 +398,19 @@
   (case Thm.tpairs_of th of
     [] => th
   | pairs =>
-    let
-      val thy = Thm.theory_of_thm th
-      val cert = Thm.cterm_of thy
-      val certT = Thm.ctyp_of thy
-      val (tyenv, tenv) = fold (Pattern.first_order_match thy) pairs (Vartab.empty, Vartab.empty)
-
-      fun mkT (v, (S, T)) = (certT (TVar (v, S)), certT T)
-      fun mk (v, (T, t)) = (cert (Var (v, Envir.subst_type tyenv T)), cert t)
-
-      val instsT = Vartab.fold (cons o mkT) tyenv []
-      val insts = Vartab.fold (cons o mk) tenv []
-    in
-      Thm.instantiate (instsT, insts) th
-    end
-    handle THM _ => th)
+      let
+        val thy = Thm.theory_of_thm th
+        val (tyenv, tenv) = fold (Pattern.first_order_match thy) pairs (Vartab.empty, Vartab.empty)
+  
+        fun mkT (v, (S, T)) = apply2 (Thm.ctyp_of thy) (TVar (v, S), T)
+        fun mk (v, (T, t)) = apply2 (Thm.cterm_of thy) (Var (v, Envir.subst_type tyenv T), t)
+  
+        val instsT = Vartab.fold (cons o mkT) tyenv []
+        val insts = Vartab.fold (cons o mk) tenv []
+      in
+        Thm.instantiate (instsT, insts) th
+      end
+      handle THM _ => th)
 
 fun is_metis_literal_genuine (_, (s, _)) =
   not (String.isPrefix class_prefix (Metis_Name.toString s))