# HG changeset patch
# User blanchet
# Date 1308669459 -7200
# Node ID 75d2e48c5d307530b3412e8922e0289895ae68d5
# Parent  13eefebbc4cbea6f4950891466820c047785368b
avoid double ASCII-fication

diff -r 13eefebbc4cb -r 75d2e48c5d30 src/HOL/Tools/ATP/atp_translate.ML
--- a/src/HOL/Tools/ATP/atp_translate.ML	Tue Jun 21 17:17:39 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_translate.ML	Tue Jun 21 17:17:39 2011 +0200
@@ -417,15 +417,19 @@
   end
 
 fun arity_clause _ _ (_, []) = []
-  | arity_clause seen n (tcons, ("HOL.type",_)::ars) =  (*ignore*)
-      arity_clause seen n (tcons,ars)
-  | arity_clause seen n (tcons, (ar as (class,_)) :: ars) =
-      if member (op =) seen class then (*multiple arities for the same tycon, class pair*)
-          make_axiom_arity_clause (tcons, lookup_const tcons ^ "_" ^ class ^ "_" ^ string_of_int n, ar) ::
-          arity_clause seen (n+1) (tcons,ars)
-      else
-          make_axiom_arity_clause (tcons, lookup_const tcons ^ "_" ^ class, ar) ::
-          arity_clause (class::seen) n (tcons,ars)
+  | arity_clause seen n (tcons, ("HOL.type", _) :: ars) =  (* ignore *)
+    arity_clause seen n (tcons, ars)
+  | arity_clause seen n (tcons, (ar as (class, _)) :: ars) =
+    if member (op =) seen class then
+      (* multiple arities for the same (tycon, class) pair *)
+      make_axiom_arity_clause (tcons,
+          lookup_const tcons ^ "___" ^ ascii_of class ^ "_" ^ string_of_int n,
+          ar) ::
+      arity_clause seen (n + 1) (tcons, ars)
+    else
+      make_axiom_arity_clause (tcons, lookup_const tcons ^ "___" ^
+                               ascii_of class, ar) ::
+      arity_clause (class :: seen) n (tcons, ars)
 
 fun multi_arity_clause [] = []
   | multi_arity_clause ((tcons, ars) :: tc_arlists) =
@@ -1592,7 +1596,7 @@
 
 fun formula_line_for_arity_clause ({name, prem_lits, concl_lits, ...}
                                    : arity_clause) =
-  Formula (arity_clause_prefix ^ ascii_of name, Axiom,
+  Formula (arity_clause_prefix ^ name, Axiom,
            mk_ahorn (map (formula_from_fo_literal o apfst not
                           o fo_literal_from_arity_literal) prem_lits)
                     (formula_from_fo_literal