# HG changeset patch
# User blanchet
# Date 1307385395 -7200
# Node ID f497a1e97d375b03f0f52d1210db6cf5acfe3b6f
# Parent  b98daa96d04352dcc4047a87e723012395a3bb53
skip "hBOOL" in new Metis path finder

diff -r b98daa96d043 -r f497a1e97d37 src/HOL/Tools/ATP/atp_translate.ML
--- a/src/HOL/Tools/ATP/atp_translate.ML	Mon Jun 06 20:36:35 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_translate.ML	Mon Jun 06 20:36:35 2011 +0200
@@ -83,6 +83,7 @@
   val type_tag_name : string
   val type_pred_name : string
   val simple_type_prefix : string
+  val prefixed_predicator_name : string
   val prefixed_app_op_name : string
   val prefixed_type_tag_name : string
   val ascii_of: string -> string
@@ -200,6 +201,7 @@
 val type_pred_name = "is"
 val simple_type_prefix = "ty_"
 
+val prefixed_predicator_name = const_prefix ^ predicator_name
 val prefixed_app_op_name = const_prefix ^ app_op_name
 val prefixed_type_tag_name = const_prefix ^ type_tag_name
 
@@ -1111,7 +1113,7 @@
                           (K (add_combterm_syms_to_table ctxt explicit_apply)))
 
 val default_sym_tab_entries : (string * sym_info) list =
-  (make_fixed_const predicator_name,
+  (prefixed_predicator_name,
    {pred_sym = true, min_ary = 1, max_ary = 1, types = []}) ::
   ([tptp_false, tptp_true]
    |> map (rpair {pred_sym = true, min_ary = 0, max_ary = 0, types = []})) @
diff -r b98daa96d043 -r f497a1e97d37 src/HOL/Tools/Metis/metis_reconstruct.ML
--- a/src/HOL/Tools/Metis/metis_reconstruct.ML	Mon Jun 06 20:36:35 2011 +0200
+++ b/src/HOL/Tools/Metis/metis_reconstruct.ML	Mon Jun 06 20:36:35 2011 +0200
@@ -536,7 +536,8 @@
       fun path_finder_MX tm [] _ = (tm, Bound 0)
         | path_finder_MX tm (p :: ps) (t as Metis_Term.Fn (s, ts)) =
           let val s = s |> unmangled_const_name in
-            if s = metis_type_tag orelse s = prefixed_type_tag_name then
+            if s = metis_predicator orelse s = prefixed_predicator_name orelse
+               s = metis_type_tag orelse s = prefixed_type_tag_name then
               path_finder_MX tm ps (nth ts p)
             else if s = metis_app_op orelse s = prefixed_app_op_name then
               let
diff -r b98daa96d043 -r f497a1e97d37 src/HOL/Tools/Metis/metis_translate.ML
--- a/src/HOL/Tools/Metis/metis_translate.ML	Mon Jun 06 20:36:35 2011 +0200
+++ b/src/HOL/Tools/Metis/metis_translate.ML	Mon Jun 06 20:36:35 2011 +0200
@@ -51,7 +51,7 @@
 val metis_name_table =
   [((tptp_equal, 2), (metis_equal, false)),
    ((tptp_old_equal, 2), (metis_equal, false)),
-   ((const_prefix ^ predicator_name, 1), (metis_predicator, false)),
+   ((prefixed_predicator_name, 1), (metis_predicator, false)),
    ((prefixed_app_op_name, 2), (metis_app_op, false)),
    ((prefixed_type_tag_name, 2), (metis_type_tag, true))]