diff -r 19000bb11ff5 -r cf7b2121ad9d src/HOL/Tools/Function/size.ML
--- a/src/HOL/Tools/Function/size.ML	Wed Aug 11 14:31:40 2010 +0200
+++ b/src/HOL/Tools/Function/size.ML	Wed Aug 11 14:31:43 2010 +0200
@@ -145,7 +145,7 @@
       |> PureThy.add_defs false
         (map (Thm.no_attributes o apsnd (Logic.mk_equals o apsnd (app fs)))
            (map Binding.name def_names ~~ (size_fns ~~ rec_combs1)))
-      ||> Theory_Target.instantiation
+      ||> Class.instantiation
            (map (#1 o snd) descr', map dest_TFree paramTs, [HOLogic.class_size])
       ||>> fold_map define_overloaded
         (def_names' ~~ map Logic.mk_equals (overloaded_size_fns ~~ map (app fs') rec_combs1))