# HG changeset patch
# User blanchet
# Date 1328182925 -3600
# Node ID 338cf53508bc0e6f5c0ba01834bc9b17b351eb71
# Parent  caf27e675dd190a276cbe7ffa1dd4462c80b27c1
only constants can be aliased

diff -r caf27e675dd1 -r 338cf53508bc src/HOL/Tools/ATP/atp_problem_generate.ML
--- 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