diff -r c6d2d23909d1 -r 1ff0f3f08a7b src/HOL/Library/SetsAndFunctions.thy
--- a/src/HOL/Library/SetsAndFunctions.thy	Fri Jan 16 08:29:11 2009 +0100
+++ b/src/HOL/Library/SetsAndFunctions.thy	Fri Jan 16 14:58:11 2009 +0100
@@ -107,26 +107,26 @@
   apply simp
   done
 
-class_interpretation set_semigroup_add: semigroup_add ["op \<oplus> :: ('a::semigroup_add) set => 'a set => 'a set"]
+interpretation set_semigroup_add!: semigroup_add "op \<oplus> :: ('a::semigroup_add) set => 'a set => 'a set"
   apply default
   apply (unfold set_plus_def)
   apply (force simp add: add_assoc)
   done
 
-class_interpretation set_semigroup_mult: semigroup_mult ["op \<otimes> :: ('a::semigroup_mult) set => 'a set => 'a set"]
+interpretation set_semigroup_mult!: semigroup_mult "op \<otimes> :: ('a::semigroup_mult) set => 'a set => 'a set"
   apply default
   apply (unfold set_times_def)
   apply (force simp add: mult_assoc)
   done
 
-class_interpretation set_comm_monoid_add: comm_monoid_add ["{0}" "op \<oplus> :: ('a::comm_monoid_add) set => 'a set => 'a set"]
+interpretation set_comm_monoid_add!: comm_monoid_add "{0}" "op \<oplus> :: ('a::comm_monoid_add) set => 'a set => 'a set"
   apply default
    apply (unfold set_plus_def)
    apply (force simp add: add_ac)
   apply force
   done
 
-class_interpretation set_comm_monoid_mult: comm_monoid_mult ["{1}" "op \<otimes> :: ('a::comm_monoid_mult) set => 'a set => 'a set"]
+interpretation set_comm_monoid_mult!: comm_monoid_mult "{1}" "op \<otimes> :: ('a::comm_monoid_mult) set => 'a set => 'a set"
   apply default
    apply (unfold set_times_def)
    apply (force simp add: mult_ac)