src/HOLCF/UpperPD.thy

 lemma upper_plus_absorb: "xs +\<sharp> xs = xs"
 apply (induct xs rule: upper_pd.principal_induct, simp)
 apply (simp add: PDPlus_absorb)
 done
 
-class_interpretation aci_upper_plus: ab_semigroup_idem_mult ["op +\<sharp>"]
-  by unfold_locales
-    (rule upper_plus_assoc upper_plus_commute upper_plus_absorb)+
+interpretation aci_upper_plus!: ab_semigroup_idem_mult "op +\<sharp>"
+  proof qed (rule upper_plus_assoc upper_plus_commute upper_plus_absorb)+
 
 lemma upper_plus_left_commute: "xs +\<sharp> (ys +\<sharp> zs) = ys +\<sharp> (xs +\<sharp> zs)"
 by (rule aci_upper_plus.mult_left_commute)
 
 lemma upper_plus_left_absorb: "xs +\<sharp> (xs +\<sharp> ys) = xs +\<sharp> ys"