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)