1.1 --- a/src/HOL/Tools/Metis/metis_reconstruct.ML	Mon Jun 06 20:36:35 2011 +0200
     1.2 +++ b/src/HOL/Tools/Metis/metis_reconstruct.ML	Mon Jun 06 20:36:35 2011 +0200
     1.3 @@ -536,7 +536,8 @@
     1.4        fun path_finder_MX tm [] _ = (tm, Bound 0)
     1.5          | path_finder_MX tm (p :: ps) (t as Metis_Term.Fn (s, ts)) =
     1.6            let val s = s |> unmangled_const_name in
     1.7 -            if s = metis_type_tag orelse s = prefixed_type_tag_name then
     1.8 +            if s = metis_predicator orelse s = prefixed_predicator_name orelse
     1.9 +               s = metis_type_tag orelse s = prefixed_type_tag_name then
    1.10                path_finder_MX tm ps (nth ts p)
    1.11              else if s = metis_app_op orelse s = prefixed_app_op_name then
    1.12                let