src/HOL/TPTP/TPTP_Proof_Reconstruction.thy

--- a/src/HOL/TPTP/TPTP_Proof_Reconstruction.thy	Fri Jul 03 16:19:45 2015 +0200
+++ b/src/HOL/TPTP/TPTP_Proof_Reconstruction.thy	Sun Jul 05 15:02:30 2015 +0200
@@ -950,8 +950,8 @@
     val tactic =
       if is_none var_opt then no_tac
       else
-        fold (curry (op APPEND)) (map (instantiate_tac (the var_opt)) skolem_cts) no_tac
-
+        fold (curry (op APPEND))
+          (map (instantiate_tac (dest_Var (Thm.term_of (the var_opt)))) skolem_cts) no_tac
   in
     tactic st
   end