diff -r a80d8ec6c998 -r 3dda49e08b9d src/HOL/Tools/Old_Datatype/old_datatype_aux.ML
--- a/src/HOL/Tools/Old_Datatype/old_datatype_aux.ML	Fri Jan 04 21:49:06 2019 +0100
+++ b/src/HOL/Tools/Old_Datatype/old_datatype_aux.ML	Fri Jan 04 23:22:53 2019 +0100
@@ -115,8 +115,8 @@
 fun split_conj_thm th =
   ((th RS conjunct1) :: split_conj_thm (th RS conjunct2)) handle THM _ => [th];
 
-val mk_conj = foldr1 (HOLogic.mk_binop @{const_name HOL.conj});
-val mk_disj = foldr1 (HOLogic.mk_binop @{const_name HOL.disj});
+val mk_conj = foldr1 (HOLogic.mk_binop \<^const_name>\<open>HOL.conj\<close>);
+val mk_disj = foldr1 (HOLogic.mk_binop \<^const_name>\<open>HOL.disj\<close>);
 
 fun app_bnds t i = list_comb (t, map Bound (i - 1 downto 0));