src/HOL/Tools/SMT/smt_solver.ML

       raise SMT_Failure.SMT (SMT_Failure.Abnormal_Termination return_code)
   in output end
 
 fun trace_assms ctxt =
   SMT_Config.trace_msg ctxt (Pretty.string_of o
-    Pretty.big_list "Assertions:" o map (Display.pretty_thm ctxt o snd))
+    Pretty.big_list "Assertions:" o map (Thm.pretty_thm ctxt o snd))
 
 fun trace_replay_data ({context = ctxt, typs, terms, ...} : SMT_Translate.replay_data) =
   let
     fun pretty_eq n p = Pretty.block [Pretty.str n, Pretty.str " = ", p]
     fun p_typ (n, T) = pretty_eq n (Syntax.pretty_typ ctxt T)