src/HOL/TPTP/TPTP_Proof_Reconstruction.thy
changeset 60642 48dd1cefb4ae
parent 60319 127c2f00ca94
child 60754 02924903a6fd
     1.1 --- a/src/HOL/TPTP/TPTP_Proof_Reconstruction.thy	Fri Jul 03 16:19:45 2015 +0200
     1.2 +++ b/src/HOL/TPTP/TPTP_Proof_Reconstruction.thy	Sun Jul 05 15:02:30 2015 +0200
     1.3 @@ -950,8 +950,8 @@
     1.4      val tactic =
     1.5        if is_none var_opt then no_tac
     1.6        else
     1.7 -        fold (curry (op APPEND)) (map (instantiate_tac (the var_opt)) skolem_cts) no_tac
     1.8 -
     1.9 +        fold (curry (op APPEND))
    1.10 +          (map (instantiate_tac (dest_Var (Thm.term_of (the var_opt)))) skolem_cts) no_tac
    1.11    in
    1.12      tactic st
    1.13    end