diff -r 273f57049bd1 -r 2f13fe48c877 Nominal-General/Nominal2_Base.thy
--- a/Nominal-General/Nominal2_Base.thy	Tue Jul 20 06:14:16 2010 +0100
+++ b/Nominal-General/Nominal2_Base.thy	Thu Jul 22 08:30:50 2010 +0200
@@ -489,7 +489,7 @@
 
 subsection {* Permutations for products *}
 
-instantiation "*" :: (pt, pt) pt
+instantiation prod :: (pt, pt) pt
 begin
 
 primrec 
@@ -504,7 +504,7 @@
 
 subsection {* Permutations for sums *}
 
-instantiation "+" :: (pt, pt) pt
+instantiation sum :: (pt, pt) pt
 begin
 
 primrec 
@@ -603,10 +603,10 @@
 instance "fun" :: (pure, pure) pure
 by default (simp add: permute_fun_def permute_pure)
 
-instance "*" :: (pure, pure) pure
+instance prod :: (pure, pure) pure
 by default (induct_tac x, simp add: permute_pure)
 
-instance "+" :: (pure, pure) pure
+instance sum :: (pure, pure) pure
 by default (induct_tac x, simp_all add: permute_pure)
 
 instance list :: (pure) pure
@@ -987,7 +987,7 @@
   shows "a \<sharp> (x, y) \<longleftrightarrow> a \<sharp> x \<and> a \<sharp> y"
   by (simp add: fresh_def supp_Pair)
 
-instance "*" :: (fs, fs) fs
+instance prod :: (fs, fs) fs
 apply default
 apply (induct_tac x)
 apply (simp add: supp_Pair finite_supp)
@@ -1011,7 +1011,7 @@
   shows "a \<sharp> Inr y \<longleftrightarrow> a \<sharp> y"
   by (simp add: fresh_def supp_Inr)
 
-instance "+" :: (fs, fs) fs
+instance sum :: (fs, fs) fs
 apply default
 apply (induct_tac x)
 apply (simp_all add: supp_Inl supp_Inr finite_supp)