# HG changeset patch
# User berghofe
# Date 1327417251 -3600
# Node ID fd21bbcbe61b32ca3798cb51389919fcacfa5eaa
# Parent  ecda235288334e51f4f3ddb8ff432891d9b7f0a4
Use lookup_size rather than Datatype.get_info in is_poly to avoid
incorrect results for datatypes on which no size function is defined

diff -r ecda23528833 -r fd21bbcbe61b src/HOL/Tools/Function/size.ML
--- a/src/HOL/Tools/Function/size.ML	Tue Jan 24 09:13:24 2012 +0100
+++ b/src/HOL/Tools/Function/size.ML	Tue Jan 24 16:00:51 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;