# HG changeset patch
# User blanchet
# Date 1307385395 -7200
# Node ID 5017d436a5720163e3842aff57ce77ec2adb0945
# Parent  29a3a1a7794d520b3871779ef1b9378563733b58
properly unmangle names in path finder

diff -r 29a3a1a7794d -r 5017d436a572 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
@@ -535,11 +535,14 @@
         | path_finder_FT tm ps t = path_finder_fail FT tm ps (SOME t)
       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_predicator orelse s = prefixed_predicator_name orelse
-               s = metis_type_tag orelse s = prefixed_type_tag_name then
+          let
+            val s = s |> perhaps (try (strip_prefix_and_unascii const_prefix
+                                       #> the #> unmangled_const_name))
+          in
+            if s = metis_predicator orelse s = predicator_name orelse
+               s = metis_type_tag orelse s = 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
+            else if s = metis_app_op orelse s = app_op_name then
               let
                 val (tm1, tm2) = dest_comb tm
                 val p' = p - (length ts - 2)