--- a/src/HOL/Tools/nat_arith.ML Wed Dec 06 19:34:59 2017 +0100
+++ b/src/HOL/Tools/nat_arith.ML Wed Dec 06 20:43:09 2017 +0100
@@ -30,11 +30,11 @@
[Conv.rewr_conv (Library.foldl (op RS) (rule0, path)),
Conv.arg_conv (Raw_Simplifier.rewrite ctxt false norm_rules)]
-fun add_atoms path (Const (@{const_name Groups.plus}, _) $ x $ y) =
+fun add_atoms path (Const (\<^const_name>\<open>Groups.plus\<close>, _) $ x $ y) =
add_atoms (add1::path) x #> add_atoms (add2::path) y
- | add_atoms path (Const (@{const_name Nat.Suc}, _) $ x) =
+ | add_atoms path (Const (\<^const_name>\<open>Nat.Suc\<close>, _) $ x) =
add_atoms (suc1::path) x
- | add_atoms _ (Const (@{const_name Groups.zero}, _)) = I
+ | add_atoms _ (Const (\<^const_name>\<open>Groups.zero\<close>, _)) = I
| add_atoms path x = cons (x, path)
fun atoms t = add_atoms [] t []