src/HOL/Tools/Metis/metis_reconstruct.ML

         | 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)) =
           (* FIXME ### what if these are mangled? *) 
           if s = metis_type_tag then
-            if p = 1 then path_finder_MX tm ps (nth ts 1)
+            if p = 0 then path_finder_MX tm ps (hd ts)
             else path_finder_fail MX tm (p :: ps) (SOME t)
           else if s = metis_app_op then
             let
               val (tm1, tm2) = dest_comb tm in
               if p = 0 then path_finder_MX tm1 ps (hd ts) ||> (fn y => y $ tm2)