src/HOL/Library/Pattern_Aliases.thy
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>