diff -r 92f56fbfbab3 -r 799437173553 src/HOL/Library/code_test.ML
--- a/src/HOL/Library/code_test.ML	Wed Oct 02 22:01:04 2019 +0200
+++ b/src/HOL/Library/code_test.ML	Fri Oct 04 15:30:52 2019 +0200
@@ -112,7 +112,7 @@
     if size line > size failureN then
       String.extract (line, size failureN, NONE)
       |> YXML.parse_body
-      |> Term_XML.Decode.term
+      |> Term_XML.Decode.term_raw
       |> dest_tuples
       |> SOME
     else NONE)