src/HOL/Algebra/Exact_Sequence.thy

 inductive_simps exact_seq_end_iff [simp]: "exact_seq ([G,H], (g # q))"
 inductive_simps exact_seq_cons_iff [simp]: "exact_seq ((G # K # H # l), (g # h # q))"
 
 abbreviation exact_seq_arrow ::
   "('a \<Rightarrow> 'a) \<Rightarrow> 'a monoid list \<times> ('a \<Rightarrow> 'a) list \<Rightarrow>  'a monoid \<Rightarrow> 'a monoid list \<times> ('a \<Rightarrow> 'a) list"
-  (\<open>(3_ / \<longlongrightarrow>\<index> _)\<close> [1000, 60])
+  (\<open>(\<open>indent=3 notation=\<open>mixfix exact_seq\<close>\<close>_ / \<longlongrightarrow>\<index> _)\<close> [1000, 60])
   where "exact_seq_arrow  f t G \<equiv> (G # (fst t), f # (snd t))"
 
 
 subsection \<open>Basic Properties\<close>