src/HOL/Tools/SMT/smt_solver.ML

   then raise SMT (Other_Failure "proof state contains the universal sort {}")
   else solver_of (Context.Proof ctxt) rm ctxt irules
 
 fun smt_filter run_remote time_limit st xrules i =
   let
-    val {context, facts, goal} = Proof.goal st
+    val {facts, goal, ...} = Proof.goal st
     val ctxt =
-      context
+      Proof.context_of st
       |> Config.put timeout (Time.toSeconds time_limit)
       |> Config.put oracle false
       |> Config.put filter_only true
     val cprop =
       Thm.cprem_of goal i