# HG changeset patch
# User blanchet
# Date 1304339308 -7200
# Node ID bb9143d7e2174e52974729197adc59c0892f73fb
# Parent  ec29be07cd9dcc8f18965657846e0124510bae88
cosmetics

diff -r ec29be07cd9d -r bb9143d7e217 src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML	Mon May 02 14:22:34 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML	Mon May 02 14:28:28 2011 +0200
@@ -504,7 +504,7 @@
     fun var s = ATerm (`I s, [])
     fun tag tm = ATerm (`make_fixed_const type_tag_name, [var "X", tm])
   in
-    Formula (helper_prefix ^ ascii_of "ti_ti", Axiom,
+    Formula (helper_prefix ^ "ti_ti", Axiom,
              AAtom (ATerm (`I "equal", [tag (tag (var "Y")), tag (var "Y")]))
              |> close_formula_universally, NONE, NONE)
   end
@@ -774,8 +774,7 @@
 
 fun decl_line_for_sym_decl s (s', _, T, pred_sym, ary) =
   let val (arg_Ts, res_T) = n_ary_strip_type ary T in
-    Decl (sym_decl_prefix ^ ascii_of s, (s, s'),
-          map mangled_type_name arg_Ts,
+    Decl (sym_decl_prefix ^ s, (s, s'), map mangled_type_name arg_Ts,
           if pred_sym then `I tptp_tff_bool_type else mangled_type_name res_T)
   end
 
@@ -792,7 +791,8 @@
       arg_Ts |> map (fn T => if n > 1 orelse is_polymorphic_type T then SOME T
                              else NONE)
   in
-    Formula (sym_decl_prefix ^ ascii_of s ^ "_" ^ string_of_int j, Axiom,
+    Formula (sym_decl_prefix ^ s ^
+             (if n > 1 then "_" ^ string_of_int j else ""), Axiom,
              CombConst ((s, s'), T, T_args)
              |> fold (curry (CombApp o swap)) bound_tms
              |> type_pred_combatom type_sys res_T