--- a/src/HOL/Tools/ATP/atp_proof_reconstruct.ML Wed Jan 02 16:32:40 2013 +0100
+++ b/src/HOL/Tools/ATP/atp_proof_reconstruct.ML Wed Jan 02 19:59:06 2013 +0100
@@ -128,10 +128,10 @@
| add_type_constraint false (cl, TVar (ix, _)) = add_var (ix, cl)
| add_type_constraint _ _ = I
-fun repair_variable_name f s =
+fun repair_var_name s =
let
fun subscript_name s n = s ^ nat_subscript n
- val s = String.map f s
+ val s = String.map Char.toLower s
in
case space_explode "_" s of
[_] => (case take_suffix Char.isDigit (String.explode s) of
@@ -240,6 +240,8 @@
end
| NONE => (* a free or schematic variable *)
let
+ fun fresh_up s =
+ [(s, ())] |> Variable.variant_frees ctxt [] |> hd |> fst
val term_ts = map (do_term [] NONE) us
val ts = term_ts @ extra_ts
val T =
@@ -253,10 +255,10 @@
case unprefix_and_unascii schematic_var_prefix s of
SOME s => Var ((s, var_index), T)
| NONE =>
- Var ((s |> textual
- ? (repair_variable_name Char.toLower
- #> Char.isLower (String.sub (s, 0)) ? Name.skolem),
- var_index), T)
+ if textual andalso not (is_tptp_variable s) then
+ Free (s |> textual ? (repair_var_name #> fresh_up), T)
+ else
+ Var ((s |> textual ? repair_var_name, var_index), T)
in list_comb (t, ts) end
in do_term [] end
@@ -301,7 +303,7 @@
(* FIXME: TFF *)
#>> quantify_over_var
(case q of AForall => forall_of | AExists => exists_of)
- (s |> textual ? repair_variable_name Char.toLower)
+ (s |> textual ? repair_var_name)
| AConn (ANot, [phi']) => do_formula (not pos) phi' #>> s_not
| AConn (c, [phi1, phi2]) =>
do_formula (pos |> c = AImplies ? not) phi1