diff -r 8a765db7e0f8 -r 25df154b8ffc src/HOL/Tools/Function/size.ML
--- a/src/HOL/Tools/Function/size.ML	Thu Dec 30 22:34:53 2010 +0100
+++ b/src/HOL/Tools/Function/size.ML	Thu Dec 30 23:42:06 2010 +0100
@@ -42,7 +42,7 @@
       NONE => Abs ("x", T, HOLogic.zero)
     | SOME t => t);
 
-fun is_poly thy (DtType (name, dts)) =
+fun is_poly thy (Datatype_Aux.DtType (name, dts)) =
       (case Datatype.get_info thy name of
          NONE => false
        | SOME _ => exists (is_poly thy) dts)