--- a/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML Tue Aug 17 16:46:43 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML Tue Aug 17 16:47:40 2010 +0200
@@ -279,7 +279,7 @@
| add_type_constraint (false, cl, TVar (ix, _)) = add_var (ix, cl)
| add_type_constraint _ = I
-fun fix_atp_variable_name f s =
+fun repair_atp_variable_name f s =
let
fun subscript_name s n = s ^ nat_subscript n
val s = String.map f s
@@ -349,10 +349,10 @@
SOME b => Var ((b, 0), T)
| NONE =>
if is_tptp_variable a then
- Var ((fix_atp_variable_name Char.toLower a, 0), T)
+ Var ((repair_atp_variable_name Char.toLower a, 0), T)
else
(* Skolem constants? *)
- Var ((fix_atp_variable_name Char.toUpper a, 0), T)
+ Var ((repair_atp_variable_name Char.toUpper a, 0), T)
in list_comb (t, ts) end
in aux (SOME HOLogic.boolT) [] end
@@ -411,7 +411,8 @@
do_formula pos (AQuant (q, xs, phi'))
#>> quantify_over_free (case q of
AForall => @{const_name All}
- | AExists => @{const_name Ex}) x
+ | AExists => @{const_name Ex})
+ (repair_atp_variable_name Char.toLower x)
| AConn (ANot, [phi']) => do_formula (not pos) phi' #>> s_not
| AConn (c, [phi1, phi2]) =>
do_formula (pos |> c = AImplies ? not) phi1
@@ -835,6 +836,7 @@
second_pass [Show] (contra_proof, [], ([], ([], []))) |> fst
in proof_top @ proof_bottom end
+(* FIXME: Still needed? Probably not. *)
val kill_duplicate_assumptions_in_proof =
let
fun relabel_facts subst =