1.1 --- a/src/HOL/TPTP/TPTP_Proof_Reconstruction.thy	Mon Mar 23 10:16:20 2015 +0100
     1.2 +++ b/src/HOL/TPTP/TPTP_Proof_Reconstruction.thy	Mon Mar 23 13:30:59 2015 +0100
     1.3 @@ -185,7 +185,7 @@
     1.4      else
     1.5        let
     1.6          fun instantiate param =
     1.7 -          (map (Rule_Insts.eres_inst_tac ctxt [((("x", 0), Position.none), param)]) thms
     1.8 +          (map (Rule_Insts.eres_inst_tac ctxt [((("x", 0), Position.none), param)] []) thms
     1.9                     |> FIRST')
    1.10          val attempts = map instantiate parameters
    1.11        in
    1.12 @@ -221,7 +221,7 @@
    1.13      else
    1.14        let
    1.15          fun instantiates param =
    1.16 -          Rule_Insts.eres_inst_tac ctxt [((("x", 0), Position.none), param)] thm
    1.17 +          Rule_Insts.eres_inst_tac ctxt [((("x", 0), Position.none), param)] [] thm
    1.18  
    1.19          val quantified_var = head_quantified_variable ctxt i st
    1.20        in
    1.21 @@ -427,7 +427,7 @@
    1.22      fun instantiate_vars ctxt vars : tactic =
    1.23        map (fn var =>
    1.24              Rule_Insts.eres_inst_tac ctxt
    1.25 -             [((("x", 0), Position.none), var)] @{thm allE} 1)
    1.26 +             [((("x", 0), Position.none), var)] [] @{thm allE} 1)
    1.27            vars
    1.28        |> EVERY
    1.29  
    1.30 @@ -673,7 +673,7 @@
    1.31      else
    1.32        let
    1.33          fun instantiate const_name =
    1.34 -          Rule_Insts.dres_inst_tac ctxt [((("sk", 0), Position.none), const_name ^ parameters)]
    1.35 +          Rule_Insts.dres_inst_tac ctxt [((("sk", 0), Position.none), const_name ^ parameters)] []
    1.36              @{thm leo2_skolemise}
    1.37          val attempts = map instantiate candidate_consts
    1.38        in
    1.39 @@ -1556,7 +1556,7 @@
    1.40  
    1.41      val tecs =
    1.42        map (fn t_s =>  (* FIXME proper context!? *)
    1.43 -       Rule_Insts.eres_inst_tac @{context} [((("x", 0), Position.none), t_s)] @{thm allE}
    1.44 +       Rule_Insts.eres_inst_tac @{context} [((("x", 0), Position.none), t_s)] [] @{thm allE}
    1.45         THEN' atac)
    1.46    in
    1.47      (TRY o etac @{thm forall_pos_lift})
    1.48 @@ -1735,7 +1735,7 @@
    1.49                member (op =)  (Term.add_frees hyp_body []) (hd hyp_prefix) then
    1.50                no_tac st
    1.51              else
    1.52 -              Rule_Insts.eres_inst_tac ctxt [((("x", 0), Position.none), "(@X. False)")]
    1.53 +              Rule_Insts.eres_inst_tac ctxt [((("x", 0), Position.none), "(@X. False)")] []
    1.54                  @{thm allE} i st
    1.55            end
    1.56       end