# HG changeset patch
# User wenzelm
# Date 1426847012 -3600
# Node ID a996f037c09dcbc62393bb896a24e2eaaa69a1dd
# Parent  cb1966f3a92b4088237496f40a32b5240ecef35b
tuned;

diff -r cb1966f3a92b -r a996f037c09d src/HOL/TPTP/TPTP_Proof_Reconstruction.thy
--- 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
 *}