src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML

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