src/HOL/Tools/Sledgehammer/sledgehammer_run.ML

       val _ = Proof.assert_backward state
       val print = if mode = Normal then Output.urgent_message else K ()
       val state =
         state |> Proof.map_context (Config.put SMT_Config.verbose debug)
       val ctxt = Proof.context_of state
-      val {facts = chained_ths, goal, ...} = Proof.goal state
+      val {facts = chained, goal, ...} = Proof.goal state
       val (_, hyp_ts, concl_t) = strip_subgoal ctxt goal i
       val ho_atp = exists (Sledgehammer_Provers.is_ho_atp ctxt) provers
       val reserved = reserved_isar_keyword_table ()
-      val css_table = clasimpset_rule_table_of ctxt
+      val css = clasimpset_rule_table_of ctxt
       val facts =
-        nearly_all_facts ctxt ho_atp fact_override reserved css_table
-                         chained_ths hyp_ts concl_t
+        nearly_all_facts ctxt ho_atp fact_override reserved css chained hyp_ts
+                         concl_t
       val _ = () |> not blocking ? kill_provers
       val _ = case find_first (not o is_prover_supported ctxt) provers of
                 SOME name => error ("No such prover: " ^ name ^ ".")
               | NONE => ()
       val _ = print "Sledgehammering..."