diff -r a80d8ec6c998 -r 3dda49e08b9d src/ZF/IntDiv.thy
--- a/src/ZF/IntDiv.thy	Fri Jan 04 21:49:06 2019 +0100
+++ b/src/ZF/IntDiv.thy	Fri Jan 04 23:22:53 2019 +0100
@@ -642,7 +642,7 @@
 apply (rule_tac u = "a" and v = "b" in negDivAlg_induct)
   apply auto
    apply (simp_all add: quorem_def)
-   txt\<open>base case: @{term "0$\<le>a$+b"}\<close>
+   txt\<open>base case: \<^term>\<open>0$\<le>a$+b\<close>\<close>
    apply (simp add: negDivAlg_eqn)
   apply (simp add: not_zless_iff_zle [THEN iff_sym])
  apply (simp add: int_0_less_mult_iff)