src/HOL/Limits.thy

   "(f ---> l) F \<longleftrightarrow> (\<forall>S. open S \<longrightarrow> l \<in> S \<longrightarrow> eventually (\<lambda>x. f x \<in> S) F)"
 
 ML {*
 structure Tendsto_Intros = Named_Thms
 (
-  val name = "tendsto_intros"
+  val name = @{binding tendsto_intros}
   val description = "introduction rules for tendsto"
 )
 *}
 
 setup Tendsto_Intros.setup