# 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)