author | bulwahn |
Wed, 25 Jan 2012 09:50:34 +0100 | |
changeset 46330 | 2ddc00f8ad7c |
parent 46329 | cf3b387ba667 (current diff) |
parent 46328 | fd21bbcbe61b (diff) |
child 46331 | f5598b604a54 |
--- 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;