--- a/src/HOL/Topological_Spaces.thy Wed Dec 06 19:34:59 2017 +0100
+++ b/src/HOL/Topological_Spaces.thy Wed Dec 06 20:43:09 2017 +0100
@@ -688,7 +688,7 @@
named_theorems tendsto_intros "introduction rules for tendsto"
setup \<open>
- Global_Theory.add_thms_dynamic (@{binding tendsto_eq_intros},
+ Global_Theory.add_thms_dynamic (\<^binding>\<open>tendsto_eq_intros\<close>,
fn context =>
Named_Theorems.get (Context.proof_of context) @{named_theorems tendsto_intros}
|> map_filter (try (fn thm => @{thm tendsto_eq_rhs} OF [thm])))