--- a/src/HOL/Library/Old_SMT/old_smt_solver.ML Fri Sep 25 20:04:25 2015 +0200
+++ b/src/HOL/Library/Old_SMT/old_smt_solver.ML Fri Sep 25 20:37:59 2015 +0200
@@ -105,7 +105,7 @@
fun trace_assms ctxt =
Old_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_recon_data ({context=ctxt, typs, terms, ...} : Old_SMT_Translate.recon) =
let
@@ -327,7 +327,7 @@
if Config.get ctxt Old_SMT_Config.trace_used_facts andalso length wthms > 0
then
tracing (Pretty.string_of (Pretty.big_list "SMT used facts:"
- (map (Display.pretty_thm ctxt o snd) wthms)))
+ (map (Thm.pretty_thm ctxt o snd) wthms)))
else ()
end