src/HOL/Tools/SMT/smt_solver.ML

         if not (Config.get ctxt SMT_Config.oracle) andalso is_some replay0
         then the replay0 outer_ctxt replay_data lines
         else oracle ()
     | (result, _) => raise SMT_Failure.SMT (SMT_Failure.Counterexample (result = Sat)))
 
-  val cfalse = Thm.cterm_of @{theory} @{prop False}
+  val cfalse = Thm.global_cterm_of @{theory} @{prop False}
 in
 
 fun add_solver ({name, class, avail, command, options, smt_options, default_max_relevant, outcome,
     parse_proof = parse_proof0, replay = replay0} : solver_config) =
   let