# HG changeset patch
# User bulwahn
# Date 1327481434 -3600
# Node ID 2ddc00f8ad7cdbf0e7f19ee3fc9bfbf8dd54fa97
# Parent  cf3b387ba66769920b8dd33f4dc38528bf1e9872# Parent  fd21bbcbe61b32ca3798cb51389919fcacfa5eaa
merged

diff -r cf3b387ba667 -r 2ddc00f8ad7c src/HOL/Tools/Function/size.ML
--- a/src/HOL/Tools/Function/size.ML	Wed Jan 25 09:32:23 2012 +0100
+++ b/src/HOL/Tools/Function/size.ML	Wed Jan 25 09:50:34 2012 +0100
@@ -41,7 +41,7 @@
     | SOME t => t);
 
 fun is_poly thy (Datatype.DtType (name, dts)) =
-      (case Datatype.get_info thy name of
+      (case lookup_size thy name of
          NONE => false
        | SOME _ => exists (is_poly thy) dts)
   | is_poly _ _ = true;