src/HOL/Prod.ML

 by (EVERY1[stac fst_conv, stac snd_conv]);
 by (rtac refl 1);
 qed "split";
 
 val split_select = prove_goalw Prod.thy [split_def] 
-	"(®(x,y). P x y) = (®xy. P (fst xy) (snd xy))" (K [rtac refl 1]);
+	"(@(x,y). P x y) = (@xy. P (fst xy) (snd xy))" (K [rtac refl 1]);
 
 Addsimps [fst_conv, snd_conv, split];
 
 goal Prod.thy "(s=t) = (fst(s)=fst(t) & snd(s)=snd(t))";
 by (res_inst_tac[("p","s")] PairE 1);