src/HOL/TPTP/TPTP_Proof_Reconstruction.thy
changeset 80866 8c67b14fdd48
parent 80849 e3a419073736
child 80910 406a85a25189
--- a/src/HOL/TPTP/TPTP_Proof_Reconstruction.thy	Wed Sep 11 23:07:18 2024 +0200
+++ b/src/HOL/TPTP/TPTP_Proof_Reconstruction.thy	Wed Sep 11 23:26:25 2024 +0200
@@ -421,8 +421,7 @@
   let
     val thy = Proof_Context.theory_of ctxt
     fun term_to_string t =
-        Print_Mode.with_modes [""]
-          (fn () => Syntax.string_of_term ctxt t) ()
+      Pretty.pure_string_of (Syntax.pretty_term ctxt t)
     val ordered_instances =
       TPTP_Reconstruct.interpret_bindings prob_name thy ordered_binds []
       |> map (snd #> term_to_string)