diff -r a80d8ec6c998 -r 3dda49e08b9d src/ZF/arith_data.ML
--- a/src/ZF/arith_data.ML	Fri Jan 04 21:49:06 2019 +0100
+++ b/src/ZF/arith_data.ML	Fri Jan 04 23:22:53 2019 +0100
@@ -24,12 +24,12 @@
 
 val iT = Ind_Syntax.iT;
 
-val zero = Const(@{const_name zero}, iT);
-val succ = Const(@{const_name succ}, iT --> iT);
+val zero = Const(\<^const_name>\<open>zero\<close>, iT);
+val succ = Const(\<^const_name>\<open>succ\<close>, iT --> iT);
 fun mk_succ t = succ $ t;
 val one = mk_succ zero;
 
-val mk_plus = FOLogic.mk_binop @{const_name Arith.add};
+val mk_plus = FOLogic.mk_binop \<^const_name>\<open>Arith.add\<close>;
 
 (*Thus mk_sum[t] yields t+#0; longer sums don't have a trailing zero*)
 fun mk_sum []        = zero
@@ -40,13 +40,13 @@
 fun long_mk_sum []        = zero
   | long_mk_sum (t :: ts) = mk_plus (t, mk_sum ts);
 
-val dest_plus = FOLogic.dest_bin @{const_name Arith.add} iT;
+val dest_plus = FOLogic.dest_bin \<^const_name>\<open>Arith.add\<close> iT;
 
 (* dest_sum *)
 
-fun dest_sum (Const(@{const_name zero},_)) = []
-  | dest_sum (Const(@{const_name succ},_) $ t) = one :: dest_sum t
-  | dest_sum (Const(@{const_name Arith.add},_) $ t $ u) = dest_sum t @ dest_sum u
+fun dest_sum (Const(\<^const_name>\<open>zero\<close>,_)) = []
+  | dest_sum (Const(\<^const_name>\<open>succ\<close>,_) $ t) = one :: dest_sum t
+  | dest_sum (Const(\<^const_name>\<open>Arith.add\<close>,_) $ t $ u) = dest_sum t @ dest_sum u
   | dest_sum tm = [tm];
 
 (*Apply the given rewrite (if present) just once*)
@@ -80,14 +80,14 @@
 (*** Use CancelNumerals simproc without binary numerals,
      just for cancellation ***)
 
-val mk_times = FOLogic.mk_binop @{const_name Arith.mult};
+val mk_times = FOLogic.mk_binop \<^const_name>\<open>Arith.mult\<close>;
 
 fun mk_prod [] = one
   | mk_prod [t] = t
   | mk_prod (t :: ts) = if t = one then mk_prod ts
                         else mk_times (t, mk_prod ts);
 
-val dest_times = FOLogic.dest_bin @{const_name Arith.mult} iT;
+val dest_times = FOLogic.dest_bin \<^const_name>\<open>Arith.mult\<close> iT;
 
 fun dest_prod t =
       let val (t,u) = dest_times t
@@ -141,15 +141,15 @@
   val find_first_coeff  = find_first_coeff []
 
   val norm_ss1 =
-    simpset_of (put_simpset ZF_ss @{context} addsimps add_0s @ add_succs @ mult_1s @ @{thms add_ac})
+    simpset_of (put_simpset ZF_ss \<^context> addsimps add_0s @ add_succs @ mult_1s @ @{thms add_ac})
   val norm_ss2 =
-    simpset_of (put_simpset ZF_ss @{context} addsimps add_0s @ mult_1s @ @{thms add_ac} @
+    simpset_of (put_simpset ZF_ss \<^context> addsimps add_0s @ mult_1s @ @{thms add_ac} @
       @{thms mult_ac} @ tc_rules @ natifys)
   fun norm_tac ctxt =
     ALLGOALS (asm_simp_tac (put_simpset norm_ss1 ctxt))
     THEN ALLGOALS (asm_simp_tac (put_simpset norm_ss2 ctxt))
   val numeral_simp_ss =
-    simpset_of (put_simpset ZF_ss @{context} addsimps add_0s @ tc_rules @ natifys)
+    simpset_of (put_simpset ZF_ss \<^context> addsimps add_0s @ tc_rules @ natifys)
   fun numeral_simp_tac ctxt =
     ALLGOALS (asm_simp_tac (put_simpset numeral_simp_ss ctxt))
   val simplify_meta_eq  = simplify_meta_eq final_rules
@@ -175,8 +175,8 @@
   struct
   open CancelNumeralsCommon
   val prove_conv = prove_conv "natless_cancel_numerals"
-  val mk_bal   = FOLogic.mk_binrel @{const_name Ordinal.lt}
-  val dest_bal = FOLogic.dest_bin @{const_name Ordinal.lt} iT
+  val mk_bal   = FOLogic.mk_binrel \<^const_name>\<open>Ordinal.lt\<close>
+  val dest_bal = FOLogic.dest_bin \<^const_name>\<open>Ordinal.lt\<close> iT
   val bal_add1 = @{thm less_add_iff} RS @{thm iff_trans}
   val bal_add2 = @{thm less_add_iff} RS @{thm iff_trans}
   fun trans_tac ctxt = gen_trans_tac ctxt @{thm iff_trans}
@@ -188,8 +188,8 @@
   struct
   open CancelNumeralsCommon
   val prove_conv = prove_conv "natdiff_cancel_numerals"
-  val mk_bal   = FOLogic.mk_binop @{const_name Arith.diff}
-  val dest_bal = FOLogic.dest_bin @{const_name Arith.diff} iT
+  val mk_bal   = FOLogic.mk_binop \<^const_name>\<open>Arith.diff\<close>
+  val dest_bal = FOLogic.dest_bin \<^const_name>\<open>Arith.diff\<close> iT
   val bal_add1 = @{thm diff_add_eq} RS @{thm trans}
   val bal_add2 = @{thm diff_add_eq} RS @{thm trans}
   fun trans_tac ctxt = gen_trans_tac ctxt @{thm trans}
@@ -199,23 +199,23 @@
 
 
 val nat_cancel =
- [Simplifier.make_simproc @{context} "nateq_cancel_numerals"
+ [Simplifier.make_simproc \<^context> "nateq_cancel_numerals"
    {lhss =
-     [@{term "l #+ m = n"}, @{term "l = m #+ n"},
-      @{term "l #* m = n"}, @{term "l = m #* n"},
-      @{term "succ(m) = n"}, @{term "m = succ(n)"}],
+     [\<^term>\<open>l #+ m = n\<close>, \<^term>\<open>l = m #+ n\<close>,
+      \<^term>\<open>l #* m = n\<close>, \<^term>\<open>l = m #* n\<close>,
+      \<^term>\<open>succ(m) = n\<close>, \<^term>\<open>m = succ(n)\<close>],
     proc = K EqCancelNumerals.proc},
-  Simplifier.make_simproc @{context} "natless_cancel_numerals"
+  Simplifier.make_simproc \<^context> "natless_cancel_numerals"
    {lhss =
-     [@{term "l #+ m < n"}, @{term "l < m #+ n"},
-      @{term "l #* m < n"}, @{term "l < m #* n"},
-      @{term "succ(m) < n"}, @{term "m < succ(n)"}],
+     [\<^term>\<open>l #+ m < n\<close>, \<^term>\<open>l < m #+ n\<close>,
+      \<^term>\<open>l #* m < n\<close>, \<^term>\<open>l < m #* n\<close>,
+      \<^term>\<open>succ(m) < n\<close>, \<^term>\<open>m < succ(n)\<close>],
     proc = K LessCancelNumerals.proc},
-  Simplifier.make_simproc @{context} "natdiff_cancel_numerals"
+  Simplifier.make_simproc \<^context> "natdiff_cancel_numerals"
    {lhss =
-     [@{term "(l #+ m) #- n"}, @{term "l #- (m #+ n)"},
-      @{term "(l #* m) #- n"}, @{term "l #- (m #* n)"},
-      @{term "succ(m) #- n"}, @{term "m #- succ(n)"}],
+     [\<^term>\<open>(l #+ m) #- n\<close>, \<^term>\<open>l #- (m #+ n)\<close>,
+      \<^term>\<open>(l #* m) #- n\<close>, \<^term>\<open>l #- (m #* n)\<close>,
+      \<^term>\<open>succ(m) #- n\<close>, \<^term>\<open>m #- succ(n)\<close>],
     proc = K DiffCancelNumerals.proc}];
 
 end;