src/HOL/Tools/Function/size.ML
changeset 46328 fd21bbcbe61b
parent 45901 cea7cd0c7e99
child 49964 4d84fe96d5cb
equal deleted inserted replaced
46327:ecda23528833 46328:fd21bbcbe61b
    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 =