author | blanchet |
Thu, 02 Feb 2012 12:42:05 +0100 | |
changeset 46399 | 338cf53508bc |
parent 46398 | caf27e675dd1 |
child 46400 | 9ce354a77908 |
--- a/src/HOL/Tools/ATP/atp_problem_generate.ML Thu Feb 02 12:42:05 2012 +0100 +++ b/src/HOL/Tools/ATP/atp_problem_generate.ML Thu Feb 02 12:42:05 2012 +0100 @@ -1541,7 +1541,7 @@ let val (head, args) = tm |> strip_iterm_comb ||> map introduce_app_ops in case head of IConst (name as (s, _), T, T_args) => - if app_op_aliases then + if app_op_aliases andalso String.isPrefix const_prefix s then let val ary = length args val name = name |> ary > min_ary_of sym_tab s ? aliased_app_op ary