src/HOL/Library/code_test.ML
changeset 69597 ff784d5a5bfb
parent 69593 3dda49e08b9d
child 69623 ef02c5e051e5
--- 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>\<open>Some :: (unit \<Rightarrow> yxml_of_term) \<Rightarrow> (unit \<Rightarrow> yxml_of_term) option\<close> $
-          (absdummy \<^typ>\<open>unit\<close> (@{const yxml_string_of_term} $
+          (absdummy \<^typ>\<open>unit\<close> (\<^const>\<open>yxml_string_of_term\<close> $
             (Const (\<^const_name>\<open>Code_Evaluation.term_of\<close>, T --> \<^typ>\<open>term\<close>) $ tuple)))
       end