fixed new path finder for type information tag

--- a/src/HOL/Tools/Metis/metis_reconstruct.ML	Tue May 31 16:38:36 2011 +0200
+++ b/src/HOL/Tools/Metis/metis_reconstruct.ML	Tue May 31 16:38:36 2011 +0200
@@ -530,7 +530,7 @@
         | 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

--- a/src/HOL/Tools/Metis/metis_translate.ML	Tue May 31 16:38:36 2011 +0200
+++ b/src/HOL/Tools/Metis/metis_translate.ML	Tue May 31 16:38:36 2011 +0200
@@ -20,9 +20,9 @@
      old_skolems : (string * term) list}
 
   val metis_equal : string
-  val metis_type_tag : string
   val metis_predicator : string
   val metis_app_op : string
+  val metis_type_tag : string
   val metis_generated_var_prefix : string
   val metis_name_table : ((string * int) * (string * bool)) list
   val reveal_old_skolem_terms : (string * term) list -> term -> term