changeset 70784 | 799437173553 |
parent 69950 | dbc2426a600d |
child 72272 | 6931ab4f1a47 |
--- 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)