# HG changeset patch
# User blanchet
# Date 1412615956 -7200
# Node ID 733b7a3277b2b0182e5cfc1b3b2ff719e5e63218
# Parent  d9892c88cb56771ec639c4a88f4eab93108f66cb
slightly nicer names

diff -r d9892c88cb56 -r 733b7a3277b2 src/HOL/Tools/ATP/atp_proof_reconstruct.ML
--- 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)