src/HOL/TPTP/TPTP_Proof_Reconstruction.thy
changeset 59755 f8d164ab0dc1
parent 59639 f596ed647018
child 59760 a996f037c09d
     1.1 --- a/src/HOL/TPTP/TPTP_Proof_Reconstruction.thy	Thu Mar 19 17:25:57 2015 +0100
     1.2 +++ b/src/HOL/TPTP/TPTP_Proof_Reconstruction.thy	Thu Mar 19 22:30:57 2015 +0100
     1.3 @@ -185,7 +185,7 @@
     1.4      else
     1.5        let
     1.6          fun instantiate param =
     1.7 -           (map (eres_inst_tac ctxt [(("x", 0), param)]) thms
     1.8 +           (map (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 -           eres_inst_tac ctxt [(("x", 0), param)] thm
    1.17 +           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), 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,8 @@
    1.31      else
    1.32        let
    1.33          fun instantiate const_name =
    1.34 -          dres_inst_tac ctxt [(("sk", 0), const_name ^ parameters)] @{thm leo2_skolemise}
    1.35 +          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          (fold (curry (op APPEND')) attempts (K no_tac)) i st
    1.40 @@ -1556,7 +1557,7 @@
    1.41  
    1.42      val tecs =
    1.43        map (fn t_s =>
    1.44 -       eres_inst_tac @{context} [(("x", 0), t_s)] @{thm allE}
    1.45 +       eres_inst_tac @{context} [((("x", 0), Position.none), t_s)] @{thm allE}
    1.46         THEN' atac)
    1.47    in
    1.48      (TRY o etac @{thm forall_pos_lift})
    1.49 @@ -1735,7 +1736,8 @@
    1.50                member (op =)  (Term.add_frees hyp_body []) (hd hyp_prefix) then
    1.51                no_tac st
    1.52              else
    1.53 -              eres_inst_tac ctxt [(("x", 0), "(@X. False)")] @{thm allE} i st
    1.54 +              eres_inst_tac ctxt [((("x", 0), Position.none), "(@X. False)")]
    1.55 +                @{thm allE} i st
    1.56            end
    1.57       end
    1.58    end