tuned;

--- a/src/HOL/TPTP/TPTP_Proof_Reconstruction.thy	Fri Mar 20 11:09:08 2015 +0100
+++ b/src/HOL/TPTP/TPTP_Proof_Reconstruction.thy	Fri Mar 20 11:23:32 2015 +0100
@@ -944,16 +944,15 @@
      end
 
     fun instantiate_tac from to =
-      Thm.instantiate ([], [(from, to)])
-      |> PRIMITIVE
+      PRIMITIVE (Thm.instantiate ([], [(from, to)]))
 
-    val tectic =
+    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
 
   in
-    tectic st
+    tactic st
   end
 *}