# HG changeset patch
# User blanchet
# Date 1306852716 -7200
# Node ID 69251cad0da039695fe4fcd1e07aa6e84b22883a
# Parent  f181d66046d4123864b08d959a5797a63a05a6dc
fixed recursive call in new path finder and (untested:) handle hAPP

diff -r f181d66046d4 -r 69251cad0da0 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
@@ -525,21 +525,29 @@
                       " isa-term: " ^  Syntax.string_of_term ctxt tm ^
                       " fol-term: " ^ Metis_Term.toString t)
       fun path_finder_New tm [] _ = (tm, Bound 0)
-        | path_finder_New tm (p :: ps) (t as Metis_Term.Fn (_, ts)) =
-          let
-            val (tm1, args) = strip_comb tm
-            val adjustment = length ts - length args
-            val p' = if adjustment > p then p else p - adjustment
-            val tm_p = nth args p'
-              handle Subscript =>
-                     raise METIS ("equality_inf",
-                                  string_of_int p ^ " adj " ^
-                                  string_of_int adjustment ^ " term " ^
-                                  Syntax.string_of_term ctxt tm)
-            val _ = trace_msg ctxt (fn () => "path_finder: " ^ string_of_int p ^
-                                  "  " ^ Syntax.string_of_term ctxt tm_p)
-            val (r, t) = path_finder_New tm_p ps t
-          in (r, list_comb (tm1, replace_item_list t p' args)) end
+        | path_finder_New tm (p :: ps) (t as Metis_Term.Fn (s, ts)) =
+          if s = metis_app_op (* FIXME ### mangled etc. *) then
+            let
+              val (tm1, tm2) = dest_comb tm in
+              if p = 0 then path_finder_New tm1 ps (hd ts) ||> (fn y => y $ tm2)
+              else path_finder_New tm2 ps (nth ts 1) ||> (fn y => tm1 $ y)
+            end
+          else
+            let
+              val (tm1, args) = strip_comb tm
+              val adjustment = length ts - length args
+              val p' = if adjustment > p then p else p - adjustment
+              val tm_p = nth args p'
+                handle Subscript =>
+                       raise METIS ("equality_inf",
+                                    string_of_int p ^ " adj " ^
+                                    string_of_int adjustment ^ " term " ^
+                                    Syntax.string_of_term ctxt tm)
+              val _ = trace_msg ctxt (fn () =>
+                  "path_finder: " ^ string_of_int p ^ "  " ^
+                  Syntax.string_of_term ctxt tm_p)
+              val (r, t) = path_finder_New tm_p ps (nth ts p)
+            in (r, list_comb (tm1, replace_item_list t p' args)) end
         | path_finder_New tm ps t =
           raise Fail ("Cannot replay Metis proof in Isabelle:\n" ^
                       "equality_inf, path_finder_New: path = " ^