diff -r c8a2755bf220 -r ff784d5a5bfb src/HOL/Library/code_test.ML --- a/src/HOL/Library/code_test.ML Sat Jan 05 17:00:43 2019 +0100 +++ b/src/HOL/Library/code_test.ML Sat Jan 05 17:24:33 2019 +0100 @@ -195,7 +195,7 @@ val T = fastype_of tuple in \<^term>\Some :: (unit \ yxml_of_term) \ (unit \ yxml_of_term) option\ $ - (absdummy \<^typ>\unit\ (@{const yxml_string_of_term} $ + (absdummy \<^typ>\unit\ (\<^const>\yxml_string_of_term\ $ (Const (\<^const_name>\Code_Evaluation.term_of\, T --> \<^typ>\term\) $ tuple))) end