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)