src/HOL/Library/Old_SMT/old_smt_solver.ML
changeset 61268 abe08fb15a12
parent 60752 b48830b670a1
child 62549 9498623b27f0
--- 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