tuned;
authorwenzelm
Fri Mar 20 11:23:32 2015 +0100 (2015-03-20)
changeset 59760a996f037c09d
parent 59759 cb1966f3a92b
child 59761 558acf0426f1
tuned;
src/HOL/TPTP/TPTP_Proof_Reconstruction.thy
     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