# HG changeset patch
# User blanchet
# Date 1306852716 -7200
# Node ID ccf1c09dea8230a637ac6de0928e3b6a377acd5f
# Parent  269300fb83d0efa64a6bdc4ae9474f50268d0f58
more robust and simpler adjustment computation

diff -r 269300fb83d0 -r ccf1c09dea82 src/HOL/Tools/ATP/atp_reconstruct.ML
--- a/src/HOL/Tools/ATP/atp_reconstruct.ML	Tue May 31 16:38:36 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_reconstruct.ML	Tue May 31 16:38:36 2011 +0200
@@ -482,7 +482,8 @@
                 case strip_prefix_and_unascii schematic_var_prefix a of
                   SOME b => Var ((b, var_index), T)
                 | NONE =>
-                  Var ((repair_variable_name Char.toLower a, var_index), T)
+                  Var ((a |> textual ? repair_variable_name Char.toLower,
+                        var_index), T)
           in list_comb (t, ts) end
   in do_term [] end
 
@@ -547,7 +548,7 @@
         #>> quantify_over_var (case q of
                                  AForall => forall_of
                                | AExists => exists_of)
-                              (repair_variable_name Char.toLower s)
+                              (s |> textual ? repair_variable_name Char.toLower)
       | AConn (ANot, [phi']) => do_formula (not pos) phi' #>> s_not
       | AConn (c, [phi1, phi2]) =>
         do_formula (pos |> c = AImplies ? not) phi1
diff -r 269300fb83d0 -r ccf1c09dea82 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
@@ -216,7 +216,7 @@
 
 fun atp_name_from_metis s =
   case AList.find (op =) metis_name_table s of
-    [(s', ary)] => (s', SOME ary)
+    (s', ary) :: _ => (s', SOME ary)
   | _ => (s, NONE)
 fun atp_term_from_metis (Metis_Term.Fn (s, tms)) =
     ATerm (fst (atp_name_from_metis s), map atp_term_from_metis tms)
@@ -525,14 +525,10 @@
                       " 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 (s, ts)) =
+        | path_finder_New tm (p :: ps) (t as Metis_Term.Fn (_, ts)) =
           let
             val (tm1, args) = strip_comb tm
-            val adjustment =
-              case atp_name_from_metis s of
-                (_, SOME _) => 0
-              | (s', NONE) =>
-                length ts - the_default 0 (Symtab.lookup sym_tab s')
+            val adjustment = length ts - length args
             val p' = if adjustment > p then p else p - adjustment
             val tm_p = nth args p'
               handle Subscript =>