src/HOL/TPTP/TPTP_Proof_Reconstruction.thy
changeset 80849 e3a419073736
parent 80846 9ed32b8a03a9
child 80866 8c67b14fdd48
--- a/src/HOL/TPTP/TPTP_Proof_Reconstruction.thy	Tue Sep 10 20:36:01 2024 +0200
+++ b/src/HOL/TPTP/TPTP_Proof_Reconstruction.thy	Wed Sep 11 12:11:47 2024 +0200
@@ -422,7 +422,7 @@
     val thy = Proof_Context.theory_of ctxt
     fun term_to_string t =
         Print_Mode.with_modes [""]
-          (fn () => Output.output_ (Syntax.string_of_term ctxt t)) ()
+          (fn () => Syntax.string_of_term ctxt t) ()
     val ordered_instances =
       TPTP_Reconstruct.interpret_bindings prob_name thy ordered_binds []
       |> map (snd #> term_to_string)