more explicit use of context and elimination of Thm.theory_of_thm, although unclear (and untested?) situations remain;

--- a/src/HOL/TPTP/TPTP_Parser/tptp_reconstruct.ML	Sun Jul 05 22:07:09 2015 +0200
+++ b/src/HOL/TPTP/TPTP_Parser/tptp_reconstruct.ML	Sun Jul 05 22:32:14 2015 +0200
@@ -1029,12 +1029,14 @@
         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
@@ -1063,14 +1065,7 @@
              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)
@@ -1157,14 +1152,16 @@
                                 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)
@@ -1183,8 +1180,7 @@
                   (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

--- a/src/HOL/TPTP/TPTP_Proof_Reconstruction_Test.thy	Sun Jul 05 22:07:09 2015 +0200
+++ b/src/HOL/TPTP/TPTP_Proof_Reconstruction_Test.thy	Sun Jul 05 22:32:14 2015 +0200
@@ -329,10 +329,8 @@
 *}
 
 ML {*
-(*given a thm, show us the axioms in its thy*)
-val axms_of_thy_of_thm =
-  Thm.theory_of_thm
-  #> ` Theory.axioms_of
+val axms_of_thy =
+  `Theory.axioms_of
   #> apsnd cterm_of
   #> swap
   #> apsnd (map snd)
@@ -351,14 +349,8 @@
   *}
 
 ML {*
-fun leo2_tac_wrap prob_name step i = fn st =>
-  let
-    val ctxt =
-      Thm.theory_of_thm st
-      |> Proof_Context.init_global
-  in
-    rtac (interpret_leo2_inference ctxt prob_name step) i st
-  end
+fun leo2_tac_wrap ctxt prob_name step i st =
+  rtac (interpret_leo2_inference ctxt prob_name step) i st
 *}
 
 (*FIXME move these examples elsewhere*)

--- a/src/HOL/TPTP/TPTP_Proof_Reconstruction_Test_Units.thy	Sun Jul 05 22:07:09 2015 +0200
+++ b/src/HOL/TPTP/TPTP_Proof_Reconstruction_Test_Units.thy	Sun Jul 05 22:32:14 2015 +0200
@@ -7,7 +7,7 @@
   - Makes use of the PolyML structure.
 *)
 
-theory TPTP_Proof_Reconstruction_Test
+theory TPTP_Proof_Reconstruction_Test_Units
 imports TPTP_Test TPTP_Proof_Reconstruction
 begin
 
@@ -482,16 +482,7 @@
              (\<not> SEU602_2_bnd_in (SEU602_2_bnd_sK7_E SV49) SEU602_2_bnd_sK2_SY17)) =
             False"
 (*FIXME this (and similar) tests are getting the "Bad background theory of goal state" error since upgrading to Isabelle2013-2.*)
-by (tactic {*fn thm =>
-  let
-    val ctxt =
-      theory_of_thm thm
-      |> Context.Theory
-      |> Context.proof_of
-  in nonfull_extcnf_combined_tac ctxt [Extuni_Func, Existential_Var] thm
-  end*})
-(*by (tactic {*nonfull_extcnf_combined_tac @{context} [Extuni_Func, Existential_Var]*})*)
-oops
+by (tactic {*nonfull_extcnf_combined_tac @{context} [Extuni_Func, Existential_Var]*})
 
 consts
   SEV405_5_bnd_sK1_SY2 :: "(TPTP_Interpret.ind \<Rightarrow> bool) \<Rightarrow> TPTP_Interpret.ind"

--- a/src/HOL/TPTP/mash_export.ML	Sun Jul 05 22:07:09 2015 +0200
+++ b/src/HOL/TPTP/mash_export.ML	Sun Jul 05 22:32:14 2015 +0200
@@ -263,8 +263,8 @@
               val suggs =
                 old_facts
                 |> filter_accessible_from th
-                |> mepo_or_mash_suggested_facts ctxt (Thm.theory_of_thm th) params max_suggs hyp_ts
-                  concl_t
+                |> mepo_or_mash_suggested_facts ctxt (Thm.theory_name_of_thm th)
+                  params max_suggs hyp_ts concl_t
                 |> map (nickname_of_thm ctxt o snd)
             in
               encode_str name ^ ": " ^ encode_strs suggs ^ "\n"
@@ -290,11 +290,11 @@
   (Options.put_default @{system_option MaSh} algorithm;
    Sledgehammer_MaSh.mash_unlearn ();
    generate_mepo_or_mash_suggestions
-     (fn ctxt => fn thy => fn params as {provers = prover :: _, ...} => fn max_suggs => fn hyp_ts =>
-          fn concl_t =>
+     (fn ctxt => fn thy_name => fn params as {provers = prover :: _, ...} =>
+          fn max_suggs => fn hyp_ts => fn concl_t =>
         tap (Sledgehammer_MaSh.mash_learn_facts ctxt params prover 2 false
           Sledgehammer_Util.one_year)
-        #> Sledgehammer_MaSh.mash_suggested_facts ctxt thy params max_suggs hyp_ts concl_t
+        #> Sledgehammer_MaSh.mash_suggested_facts ctxt thy_name params max_suggs hyp_ts concl_t
         #> fst))
 
 fun generate_mesh_suggestions max_suggs mash_file_name mepo_file_name mesh_file_name =

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Sun Jul 05 22:07:09 2015 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Sun Jul 05 22:32:14 2015 +0200
@@ -66,7 +66,7 @@
   val weight_facts_steeply : 'a list -> ('a * real) list
   val find_mash_suggestions : Proof.context -> int -> string list -> ('a * thm) list ->
     ('a * thm) list -> ('a * thm) list -> ('a * thm) list * ('a * thm) list
-  val mash_suggested_facts : Proof.context -> theory -> params -> int -> term list -> term ->
+  val mash_suggested_facts : Proof.context -> string -> params -> int -> term list -> term ->
     raw_fact list -> fact list * fact list
 
   val mash_unlearn : unit -> unit
@@ -1145,9 +1145,8 @@
     (mesh_facts (eq_snd (gen_eq_thm ctxt)) max_facts mess, unknown)
   end
 
-fun mash_suggested_facts ctxt thy ({debug, ...} : params) max_suggs hyp_ts concl_t facts =
+fun mash_suggested_facts ctxt thy_name ({debug, ...} : params) max_suggs hyp_ts concl_t facts =
   let
-    val thy_name = Context.theory_name thy
     val algorithm = the_mash_algorithm ()
 
     val facts = facts
@@ -1167,7 +1166,7 @@
       peek_state ctxt
 
     val goal_feats0 =
-      features_of ctxt (Context.theory_name thy) (Local, General) (concl_t :: hyp_ts)
+      features_of ctxt thy_name (Local, General) (concl_t :: hyp_ts)
     val chained_feats = chained
       |> map (rpair 1.0)
       |> map (chained_or_extra_features_of chained_feature_factor)
@@ -1513,7 +1512,7 @@
     [("", [])]
   else
     let
-      val thy = Proof_Context.theory_of ctxt
+      val thy_name = Context.theory_name (Proof_Context.theory_of ctxt)
 
       fun maybe_launch_thread exact min_num_facts_to_learn =
         if not (Async_Manager_Legacy.has_running_threads MaShN) andalso
@@ -1576,8 +1575,8 @@
          |> weight_facts_steeply, [])
 
       fun mash () =
-        mash_suggested_facts ctxt thy params (generous_max_suggestions max_facts) hyp_ts concl_t
-          facts
+        mash_suggested_facts ctxt thy_name params
+          (generous_max_suggestions max_facts) hyp_ts concl_t facts
         |>> weight_facts_steeply
 
       val mess =