src/HOL/Tools/ATP/atp_proof_reconstruct.ML

 fun add_var (key, z) = Vartab.map_default (key, []) (cons z)
 fun add_type_constraint false (cl, TFree (a ,_)) = add_var ((a, ~1), cl)
   | add_type_constraint false (cl, TVar (ix, _)) = add_var (ix, cl)
   | add_type_constraint _ _ = I
 
-fun repair_var_name_raw s =
-  let
-    fun subscript_name s n = s ^ nat_subscript n
-    val s = s |> String.map Char.toLower
-  in
-    (case space_explode "_" s of
-      [_] =>
-      (case take_suffix Char.isDigit (String.explode s) of
-        (cs1 as _ :: _, cs2 as _ :: _) =>
-        subscript_name (String.implode cs1) (the (Int.fromString (String.implode cs2)))
-      | (_, _) => s)
-    | [s1, s2] => (case Int.fromString s2 of SOME n => subscript_name s1 n | NONE => s)
-    | _ => s)
-  end
-
-fun repair_var_name textual s =
+fun repair_var_name s =
   (case unprefix_and_unascii schematic_var_prefix s of
-    SOME s => s
-  | NONE => s |> textual ? repair_var_name_raw)
+    SOME s' => s'
+  | NONE => s)
 
 (* The number of type arguments of a constant, zero if it's monomorphic. For (instances of) Skolem
    pseudoconstants, this information is encoded in the constant name. *)
 fun robust_const_num_type_args thy s =
   if String.isPrefix skolem_const_prefix s then

     fun do_term opt_T u =
       (case u of
         AAbs (((var, ty), term), []) =>
         let
           val typ = typ_of_atp_type ctxt ty
-          val var_name = repair_var_name true var
+          val var_name = repair_var_name var
           val tm = do_term NONE term
         in quantify_over_var true lambda' var_name typ tm end
       | ATerm ((s, tys), us) =>
         if s = ""
         then error "Isar proof reconstruction failed because the ATP proof \

                     | _ => Type_Infer.anyT @{sort type}))
               val t =
                 (case unprefix_and_unascii fixed_var_prefix s of
                   SOME s => Free (s, T)
                 | NONE =>
-                  if not (is_tptp_variable s) then Free (s |> repair_var_name_raw |> fresh_up, T)
-                  else Var ((repair_var_name true s, var_index), T))
+                  if not (is_tptp_variable s) then Free (s |> fresh_up, T)
+                  else Var ((repair_var_name s, var_index), T))
             in list_comb (t, ts) end))
   in do_term end
 
 (* First-order translation. No types are known for variables. "Type_Infer.anyT @{sort type}"
    should allow them to be inferred. *)

               val t =
                 (case unprefix_and_unascii fixed_var_prefix s of
                   SOME s => Free (s, T)
                 | NONE =>
                   if textual andalso not (is_tptp_variable s) then
-                    Free (s |> textual ? (repair_var_name_raw #> fresh_up), T)
+                    Free (s |> textual ? fresh_up, T)
                   else
-                    Var ((repair_var_name textual s, var_index), T))
+                    Var ((repair_var_name s, var_index), T))
             in list_comb (t, ts) end))
   in do_term [] end
 
 fun term_of_atp ctxt (ATP_Problem.THF _) type_enc =
     if ATP_Problem_Generate.is_type_enc_higher_order type_enc then K (term_of_atp_ho ctxt)

         AQuant (_, [], phi) => do_formula pos phi
       | AQuant (q, (s, _) :: xs, phi') =>
         do_formula pos (AQuant (q, xs, phi'))
         (* FIXME: TFF *)
         #>> quantify_over_var textual (case q of AForall => forall_of | AExists => exists_of)
-          (repair_var_name textual s) dummyT
+          (repair_var_name s) dummyT
       | AConn (ANot, [phi']) => do_formula (not pos) phi' #>> s_not
       | AConn (c, [phi1, phi2]) =>
         do_formula (pos |> c = AImplies ? not) phi1
         ##>> do_formula pos phi2
         #>> (case c of