src/HOL/Library/Old_SMT/old_smt_solver.ML

             is_real_cex = (result = Sat),
             free_constraints = ts,
             const_defs = us})
         end)
 
-  val cfalse = Thm.global_cterm_of @{theory} (@{const Trueprop} $ @{const False})
+  val cfalse = Thm.cterm_of @{context} (@{const Trueprop} $ @{const False})
 in
 
 fun add_solver cfg =
   let
     val {name, class, avail, command, options, default_max_relevant,

 fun check_topsorts ctxt iwthms = map (apsnd (apsnd (check_topsort ctxt))) iwthms
 
 
 (* filter *)
 
-val cnot = Thm.global_cterm_of @{theory} @{const Not}
+val cnot = Thm.cterm_of @{context} @{const Not}
 
 fun mk_result outcome xrules = { outcome = outcome, used_facts = xrules }
 
 type 'a smt_filter_data = ('a * thm) list * ((int * thm) list * Proof.context)