diff -r e191b400a8e0 -r f94fb13ecbb3 src/HOL/Tools/Function/size.ML
--- a/src/HOL/Tools/Function/size.ML	Mon Nov 30 11:42:48 2009 +0100
+++ b/src/HOL/Tools/Function/size.ML	Mon Nov 30 11:42:49 2009 +0100
@@ -13,7 +13,7 @@
 structure Size: SIZE =
 struct
 
-open DatatypeAux;
+open Datatype_Aux;
 
 structure SizeData = Theory_Data
 (
@@ -177,7 +177,7 @@
     fun gen_mk_size_eq p size_of size_ofp size_const T (cname, cargs) =
       let
         val Ts = map (typ_of_dtyp descr sorts) cargs;
-        val tnames = Name.variant_list f_names (DatatypeProp.make_tnames Ts);
+        val tnames = Name.variant_list f_names (Datatype_Prop.make_tnames Ts);
         val ts = map_filter (fn (sT as (s, T), dt) =>
           Option.map (fn sz => sz $ Free sT)
             (if p dt then size_of_type size_of extra_size size_ofp T