changeset 80874 | 9af593e9e454 |
parent 80820 | db114ec720cb |
child 80914 | d97fdabd9e2b |
--- a/src/HOL/Library/Pattern_Aliases.thy Thu Sep 12 15:09:07 2024 +0200 +++ b/src/HOL/Library/Pattern_Aliases.thy Thu Sep 12 19:46:08 2024 +0200 @@ -199,8 +199,8 @@ val actual = @{thm test_2.simps(1)} |> Thm.prop_of - |> Syntax.string_of_term \<^context> - |> Protocol_Message.clean_output + |> Syntax.pretty_term \<^context> + |> Pretty.pure_string_of val expected = "test_2 (?y # (?y' # ?ys =: x') =: x) = x @ x' @ x'" in \<^assert> (actual = expected) end \<close>