1.1 --- a/src/HOL/Tools/ATP/atp_translate.ML	Mon Jun 06 20:36:35 2011 +0200
     1.2 +++ b/src/HOL/Tools/ATP/atp_translate.ML	Mon Jun 06 20:36:35 2011 +0200
     1.3 @@ -83,6 +83,7 @@
     1.4    val type_tag_name : string
     1.5    val type_pred_name : string
     1.6    val simple_type_prefix : string
     1.7 +  val prefixed_predicator_name : string
     1.8    val prefixed_app_op_name : string
     1.9    val prefixed_type_tag_name : string
    1.10    val ascii_of: string -> string
    1.11 @@ -200,6 +201,7 @@
    1.12  val type_pred_name = "is"
    1.13  val simple_type_prefix = "ty_"
    1.14  
    1.15 +val prefixed_predicator_name = const_prefix ^ predicator_name
    1.16  val prefixed_app_op_name = const_prefix ^ app_op_name
    1.17  val prefixed_type_tag_name = const_prefix ^ type_tag_name
    1.18  
    1.19 @@ -1111,7 +1113,7 @@
    1.20                            (K (add_combterm_syms_to_table ctxt explicit_apply)))
    1.21  
    1.22  val default_sym_tab_entries : (string * sym_info) list =
    1.23 -  (make_fixed_const predicator_name,
    1.24 +  (prefixed_predicator_name,
    1.25     {pred_sym = true, min_ary = 1, max_ary = 1, types = []}) ::
    1.26    ([tptp_false, tptp_true]
    1.27     |> map (rpair {pred_sym = true, min_ary = 0, max_ary = 0, types = []})) @

     2.1 --- a/src/HOL/Tools/Metis/metis_reconstruct.ML	Mon Jun 06 20:36:35 2011 +0200
     2.2 +++ b/src/HOL/Tools/Metis/metis_reconstruct.ML	Mon Jun 06 20:36:35 2011 +0200
     2.3 @@ -536,7 +536,8 @@
     2.4        fun path_finder_MX tm [] _ = (tm, Bound 0)
     2.5          | path_finder_MX tm (p :: ps) (t as Metis_Term.Fn (s, ts)) =
     2.6            let val s = s |> unmangled_const_name in
     2.7 -            if s = metis_type_tag orelse s = prefixed_type_tag_name then
     2.8 +            if s = metis_predicator orelse s = prefixed_predicator_name orelse
     2.9 +               s = metis_type_tag orelse s = prefixed_type_tag_name then
    2.10                path_finder_MX tm ps (nth ts p)
    2.11              else if s = metis_app_op orelse s = prefixed_app_op_name then
    2.12                let

     3.1 --- a/src/HOL/Tools/Metis/metis_translate.ML	Mon Jun 06 20:36:35 2011 +0200
     3.2 +++ b/src/HOL/Tools/Metis/metis_translate.ML	Mon Jun 06 20:36:35 2011 +0200
     3.3 @@ -51,7 +51,7 @@
     3.4  val metis_name_table =
     3.5    [((tptp_equal, 2), (metis_equal, false)),
     3.6     ((tptp_old_equal, 2), (metis_equal, false)),
     3.7 -   ((const_prefix ^ predicator_name, 1), (metis_predicator, false)),
     3.8 +   ((prefixed_predicator_name, 1), (metis_predicator, false)),
     3.9     ((prefixed_app_op_name, 2), (metis_app_op, false)),
    3.10     ((prefixed_type_tag_name, 2), (metis_type_tag, true))]
    3.11