src/HOL/TPTP/TPTP_Proof_Reconstruction.thy
changeset 59760 a996f037c09d
parent 59755 f8d164ab0dc1
child 59763 56d2c357e6b5
     1.1 --- a/src/HOL/TPTP/TPTP_Proof_Reconstruction.thy	Fri Mar 20 11:09:08 2015 +0100
     1.2 +++ b/src/HOL/TPTP/TPTP_Proof_Reconstruction.thy	Fri Mar 20 11:23:32 2015 +0100
     1.3 @@ -944,16 +944,15 @@
     1.4       end
     1.5  
     1.6      fun instantiate_tac from to =
     1.7 -      Thm.instantiate ([], [(from, to)])
     1.8 -      |> PRIMITIVE
     1.9 +      PRIMITIVE (Thm.instantiate ([], [(from, to)]))
    1.10  
    1.11 -    val tectic =
    1.12 +    val tactic =
    1.13        if is_none var_opt then no_tac
    1.14        else
    1.15          fold (curry (op APPEND)) (map (instantiate_tac (the var_opt)) skolem_cts) no_tac
    1.16  
    1.17    in
    1.18 -    tectic st
    1.19 +    tactic st
    1.20    end
    1.21  *}
    1.22