# HG changeset patch
# User blanchet
# Date 1306852716 -7200
# Node ID 6ec2a3c7b69ea43b9f283b77242f2bc58a3ec29a
# Parent  bb0ceef7d39fad12f9b6f864c9bbef19b4916c98
fixed new path finder for type information tag

diff -r bb0ceef7d39f -r 6ec2a3c7b69e src/HOL/Tools/Metis/metis_reconstruct.ML
--- 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
diff -r bb0ceef7d39f -r 6ec2a3c7b69e src/HOL/Tools/Metis/metis_translate.ML
--- 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