diff -r ae634fad947e -r 18b41bba42b5 src/HOL/Tools/Function/size.ML
--- a/src/HOL/Tools/Function/size.ML	Thu Jan 28 11:48:43 2010 +0100
+++ b/src/HOL/Tools/Function/size.ML	Thu Jan 28 11:48:49 2010 +0100
@@ -25,7 +25,7 @@
 
 val lookup_size = SizeData.get #> Symtab.lookup;
 
-fun plus (t1, t2) = Const ("HOL.plus_class.plus",
+fun plus (t1, t2) = Const (@{const_name Algebras.plus},
   HOLogic.natT --> HOLogic.natT --> HOLogic.natT) $ t1 $ t2;
 
 fun size_of_type f g h (T as Type (s, Ts)) =