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