1.1 --- a/src/HOL/Tools/ATP/atp_reconstruct.ML	Tue May 31 16:38:36 2011 +0200
     1.2 +++ b/src/HOL/Tools/ATP/atp_reconstruct.ML	Tue May 31 16:38:36 2011 +0200
     1.3 @@ -482,7 +482,8 @@
     1.4                  case strip_prefix_and_unascii schematic_var_prefix a of
     1.5                    SOME b => Var ((b, var_index), T)
     1.6                  | NONE =>
     1.7 -                  Var ((repair_variable_name Char.toLower a, var_index), T)
     1.8 +                  Var ((a |> textual ? repair_variable_name Char.toLower,
     1.9 +                        var_index), T)
    1.10            in list_comb (t, ts) end
    1.11    in do_term [] end
    1.12  
    1.13 @@ -547,7 +548,7 @@
    1.14          #>> quantify_over_var (case q of
    1.15                                   AForall => forall_of
    1.16                                 | AExists => exists_of)
    1.17 -                              (repair_variable_name Char.toLower s)
    1.18 +                              (s |> textual ? repair_variable_name Char.toLower)
    1.19        | AConn (ANot, [phi']) => do_formula (not pos) phi' #>> s_not
    1.20        | AConn (c, [phi1, phi2]) =>
    1.21          do_formula (pos |> c = AImplies ? not) phi1

     2.1 --- a/src/HOL/Tools/Metis/metis_reconstruct.ML	Tue May 31 16:38:36 2011 +0200
     2.2 +++ b/src/HOL/Tools/Metis/metis_reconstruct.ML	Tue May 31 16:38:36 2011 +0200
     2.3 @@ -216,7 +216,7 @@
     2.4  
     2.5  fun atp_name_from_metis s =
     2.6    case AList.find (op =) metis_name_table s of
     2.7 -    [(s', ary)] => (s', SOME ary)
     2.8 +    (s', ary) :: _ => (s', SOME ary)
     2.9    | _ => (s, NONE)
    2.10  fun atp_term_from_metis (Metis_Term.Fn (s, tms)) =
    2.11      ATerm (fst (atp_name_from_metis s), map atp_term_from_metis tms)
    2.12 @@ -525,14 +525,10 @@
    2.13                        " isa-term: " ^  Syntax.string_of_term ctxt tm ^
    2.14                        " fol-term: " ^ Metis_Term.toString t)
    2.15        fun path_finder_New tm [] _ = (tm, Bound 0)
    2.16 -        | path_finder_New tm (p :: ps) (t as Metis_Term.Fn (s, ts)) =
    2.17 +        | path_finder_New tm (p :: ps) (t as Metis_Term.Fn (_, ts)) =
    2.18            let
    2.19              val (tm1, args) = strip_comb tm
    2.20 -            val adjustment =
    2.21 -              case atp_name_from_metis s of
    2.22 -                (_, SOME _) => 0
    2.23 -              | (s', NONE) =>
    2.24 -                length ts - the_default 0 (Symtab.lookup sym_tab s')
    2.25 +            val adjustment = length ts - length args
    2.26              val p' = if adjustment > p then p else p - adjustment
    2.27              val tm_p = nth args p'
    2.28                handle Subscript =>