src/HOL/Nominal/Examples/Class1.thy

--- a/src/HOL/Nominal/Examples/Class1.thy	Tue Feb 13 14:24:50 2018 +0100
+++ b/src/HOL/Nominal/Examples/Class1.thy	Thu Feb 15 12:11:00 2018 +0100
@@ -5165,7 +5165,7 @@
 abbreviation
  a_star_redu :: "trm \<Rightarrow> trm \<Rightarrow> bool" ("_ \<longrightarrow>\<^sub>a* _" [100,100] 100)
 where
-  "M \<longrightarrow>\<^sub>a* M' \<equiv> (a_redu)^** M M'"
+  "M \<longrightarrow>\<^sub>a* M' \<equiv> (a_redu)\<^sup>*\<^sup>* M M'"
 
 lemma a_starI:
   assumes a: "M \<longrightarrow>\<^sub>a M'"