418 (* True if the constant ever appears outside of the top-level position in |
418 (* True if the constant ever appears outside of the top-level position in |
419 literals, or if it appears with different arities (e.g., because of different |
419 literals, or if it appears with different arities (e.g., because of different |
420 type instantiations). If false, the constant always receives all of its |
420 type instantiations). If false, the constant always receives all of its |
421 arguments and is used as a predicate. *) |
421 arguments and is used as a predicate. *) |
422 fun is_predicate NONE s = |
422 fun is_predicate NONE s = |
423 s = "equal" orelse String.isPrefix type_const_prefix s orelse |
423 s = "equal" orelse s = "$false" orelse s = "$true" orelse |
424 String.isPrefix class_prefix s |
424 String.isPrefix type_const_prefix s orelse String.isPrefix class_prefix s |
425 | is_predicate (SOME the_const_tab) s = |
425 | is_predicate (SOME the_const_tab) s = |
426 case Symtab.lookup the_const_tab s of |
426 case Symtab.lookup the_const_tab s of |
427 SOME {min_arity, max_arity, sub_level} => |
427 SOME {min_arity, max_arity, sub_level} => |
428 not sub_level andalso min_arity = max_arity |
428 not sub_level andalso min_arity = max_arity |
429 | NONE => false |
429 | NONE => false |