diff -r 845883bd3a6b -r 9200b36280c0 src/HOL/Tools/function_package/size.ML
--- a/src/HOL/Tools/function_package/size.ML	Thu Nov 29 07:55:46 2007 +0100
+++ b/src/HOL/Tools/function_package/size.ML	Thu Nov 29 17:08:26 2007 +0100
@@ -38,7 +38,7 @@
     val n = Sign.arity_number thy tyco;
   in
     thy
-    |> Class.prove_instance (Class.intro_classes_tac [])
+    |> Instance.prove_instance (Class.intro_classes_tac [])
         [(tyco, replicate n HOLogic.typeS, [HOLogic.class_size])] []
     |> snd
   end