slightly nicer names

--- a/src/HOL/Tools/ATP/atp_proof_reconstruct.ML	Mon Oct 06 19:19:16 2014 +0200
+++ b/src/HOL/Tools/ATP/atp_proof_reconstruct.ML	Mon Oct 06 19:19:16 2014 +0200
@@ -133,7 +133,14 @@
 
 fun var_name_of_typ (Type (@{type_name fun}, [_, T])) =
     if body_type T = HOLogic.boolT then "p" else "f"
-  | var_name_of_typ (Type (@{type_name set}, [T])) = single_letter true (var_name_of_typ T)
+  | var_name_of_typ (Type (@{type_name set}, [T])) =
+    let
+      fun default () = single_letter true (var_name_of_typ T)
+    in
+      (case T of
+        Type (s, [T1, T2]) => if String.isSuffix "prod" s andalso T1 = T2 then "r" else default ()
+      | _ => default ())
+    end
   | var_name_of_typ (Type (s, Ts)) =
     if String.isSuffix "list" s then var_name_of_typ (the_single Ts) ^ "s"
     else single_letter false (Long_Name.base_name s)