| changeset 46328 | fd21bbcbe61b |
| parent 45901 | cea7cd0c7e99 |
| child 49964 | 4d84fe96d5cb |
--- 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;