src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML

   val extra_feature_factor : real
   val weight_facts_smoothly : 'a list -> ('a * real) list
   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
   val mash_learn_proof : Proof.context -> params -> term -> ('a * thm) list -> thm list -> unit
   val mash_learn_facts : Proof.context -> params -> string -> int -> bool -> Time.time ->

       |> fold (subtract (eq_snd Thm.eq_thm_prop)) [unknown_chained, unknown_proximate]
   in
     (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 =
-  let
-    val thy_name = Context.theory_name thy
+fun mash_suggested_facts ctxt thy_name ({debug, ...} : params) max_suggs hyp_ts concl_t facts =
+  let
     val algorithm = the_mash_algorithm ()
 
     val facts = facts
       |> rev_sort_list_prefix (crude_thm_ord ctxt o apply2 snd)
         (Int.max (num_extra_feature_facts, max_proximity_facts))

 
     val {access_G, xtabs = ((num_facts, fact_tab), (num_feats, feat_tab)), ffds, freqs, ...} =
       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)
       |> rpair [] |-> fold (union (eq_fst (op =)))
     val extra_feats = facts

     [("", map fact_of_raw_fact facts)]
   else if max_facts <= 0 orelse null facts then
     [("", [])]
   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
            Time.toSeconds timeout >= min_secs_for_learning then
           let val timeout = time_mult learn_timeout_slack timeout in

       fun mepo () =
         (mepo_suggested_facts ctxt params max_facts NONE hyp_ts concl_t unique_facts
          |> 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 =
         (* the order is important for the "case" expression below *)
         [] |> effective_fact_filter <> mepoN ? cons (mash_weight, mash)