equal
deleted
inserted
replaced
39 and size_of_type' f g h T = (case size_of_type f g h T of |
39 and size_of_type' f g h T = (case size_of_type f g h T of |
40 NONE => Abs ("x", T, HOLogic.zero) |
40 NONE => Abs ("x", T, HOLogic.zero) |
41 | SOME t => t); |
41 | SOME t => t); |
42 |
42 |
43 fun is_poly thy (Datatype.DtType (name, dts)) = |
43 fun is_poly thy (Datatype.DtType (name, dts)) = |
44 (case Datatype.get_info thy name of |
44 (case lookup_size thy name of |
45 NONE => false |
45 NONE => false |
46 | SOME _ => exists (is_poly thy) dts) |
46 | SOME _ => exists (is_poly thy) dts) |
47 | is_poly _ _ = true; |
47 | is_poly _ _ = true; |
48 |
48 |
49 fun constrs_of thy name = |
49 fun constrs_of thy name = |