src/HOL/SMT/Tools/smt_solver.ML

 structure SMT_Solver: SMT_SOLVER =
 struct
 
 exception SMT_COUNTEREXAMPLE of bool * term list
 
-val theory_of = Context.cases I ProofContext.theory_of
-
 
 datatype interface = Interface of {
   normalize: SMT_Normalize.config list,
   translate: SMT_Translate.config }
 

 )
 
 val solver_name_of = snd o SelectedSolver.get
 
 fun select_solver name gen =
-  if is_none (lookup_solver (theory_of gen) name)
+  if is_none (lookup_solver (Context.theory_of gen) name)
   then error ("SMT solver not registered: " ^ quote name)
   else SelectedSolver.map (K (serial (), name)) gen
 
 fun raw_solver_of gen =
-  (case lookup_solver (theory_of gen) (solver_name_of gen) of
+  (case lookup_solver (Context.theory_of gen) (solver_name_of gen) of
     NONE => error "No SMT solver selected"
   | SOME (s, _) => s)
 
 val solver_of = gen_solver o raw_solver_of
 

   setup_trace
 
 fun print_setup gen =
   let
     val t = string_of_int (Config.get_generic gen timeout)
-    val names = sort string_ord (all_solver_names_of (theory_of gen))
+    val names = sort string_ord (all_solver_names_of (Context.theory_of gen))
     val ns = if null names then [no_solver] else names
     val take_info = (fn (_, []) => NONE | info => SOME info)
     val infos =
-      theory_of gen
+      Context.theory_of gen
       |> Symtab.dest o Solvers.get
       |> map_filter (fn (n, (_, info)) => take_info (n, info gen))
       |> sort (prod_ord string_ord (K EQUAL))
       |> map (fn (n, ps) => Pretty.big_list (n ^ ":") ps)
   in