--- 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