--- 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
--- 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 =>