src/HOL/TPTP/TPTP_Parser/tptp_reconstruct.ML

     fun skel_to_naive_tactic_dbg prover_tac ctxt prob_name skel (memo : (string * (thm * tactic) option) list) =
       let
         val thy = Proof_Context.theory_of ctxt
         val pannot = get_pannot_of_prob thy prob_name
 
+(* FIXME !???!
         fun rtac_wrap thm_f i = fn st =>
           let
             val thy = Thm.theory_of_thm st
           in
             rtac (thm_f thy) i st
           end
+*)
 
         (*Some nodes don't have an inference name, such as the conjecture,
           definitions and axioms. Such nodes shouldn't appear in the
           skeleton.*)
         fun inference_name_of_node node =

           (* TimeLimit.timeLimit (Time.fromSeconds 5) *)
           (fn ctxt' =>
              let
                fun thm ctxt'' = prover_tac ctxt'' prob_name (hd skel |> stock_to_string)
                val reconstructed_inference = thm ctxt'
-               val rec_inf_tac = fn st =>
-                 let
-                   val ctxt =
-                     Thm.theory_of_thm st
-                     |> Proof_Context.init_global
-                 in
-                   HEADGOAL (rtac (thm ctxt)) st
-                 end
+               fun rec_inf_tac st = HEADGOAL (rtac (thm ctxt')) st
              in (reconstructed_inference,
                  rec_inf_tac)
              end)
         fun ignore_interpretation_exn f x = SOME (f x)
           handle

                                      (NONE, ctxt)
                                     )
                                 else
                                   let
                                     val maybe_thm = ignore_interpretation_exn try_make_step ctxt
+(* FIXME !???!
                                     val ctxt' =
                                       if is_some maybe_thm then
                                         the maybe_thm
                                         |> #1
                                         |> Thm.theory_of_thm |> Proof_Context.init_global
                                       else ctxt
+*)
                                   in
-                                    (maybe_thm, ctxt')
+                                    (maybe_thm, ctxt)
                                   end
                           in (thm, (node, thm) :: memo, ctxt') end
                       | SOME maybe_thm => (maybe_thm, memo, ctxt)
                 in
                   (Annotated_step (node, inference_name),

                       | SOME binding => Global_Theory.get_thm thy (Binding.name_of binding)
                 in
                   (hd skel,
                    Thm.prop_of (def_thm thy)
                    |> SOME,
-                   SOME (def_thm thy,
-                         HEADGOAL (rtac_wrap def_thm))) :: rest memo ctxt
+                   SOME (def_thm thy, HEADGOAL (rtac (def_thm thy)))) :: rest memo ctxt
                 end
             | Axiom n =>
                 let
                   val ax_thm =
                     case AList.lookup (op =) (#axs pannot) n of