equal
deleted
inserted
replaced
72 overloaded (i.e., that has one uniform definition), needless clutter is |
72 overloaded (i.e., that has one uniform definition), needless clutter is |
73 generated; if it returns "false" for an overloaded constant, the ATP gets a |
73 generated; if it returns "false" for an overloaded constant, the ATP gets a |
74 license to do unsound reasoning if the type system is "overloaded_args". *) |
74 license to do unsound reasoning if the type system is "overloaded_args". *) |
75 fun is_overloaded thy s = |
75 fun is_overloaded thy s = |
76 not (!precise_overloaded_args) orelse |
76 not (!precise_overloaded_args) orelse |
|
77 s = @{const_name finite} orelse |
77 (s <> @{const_name HOL.eq} andalso |
78 (s <> @{const_name HOL.eq} andalso |
78 length (Defs.specifications_of (Theory.defs_of thy) s) > 1) |
79 length (Defs.specifications_of (Theory.defs_of thy) s) > 1) |
79 |
80 |
80 fun needs_type_args thy type_sys s = |
81 fun needs_type_args thy type_sys s = |
81 case type_sys of |
82 case type_sys of |