# HG changeset patch
# User blanchet
# Date 1368023882 -7200
# Node ID 16f3b9d4e515adc472afbbb31d82e407408cda74
# Parent  097b191d1f0de1f2a005a06da87aff05fe7834de
proper unmangling -- the bug is visible when "uncurried_aliases" is enabled with Alt-Ergo or Poly. SPASS

diff -r 097b191d1f0d -r 16f3b9d4e515 src/HOL/Tools/ATP/atp_problem_generate.ML
--- a/src/HOL/Tools/ATP/atp_problem_generate.ML	Wed May 08 15:47:19 2013 +0200
+++ b/src/HOL/Tools/ATP/atp_problem_generate.ML	Wed May 08 16:38:02 2013 +0200
@@ -551,7 +551,7 @@
   in ary oo robust_const_type end
 
 (* This function only makes sense if "T" is as general as possible. *)
-fun robust_const_typargs thy (s, T) =
+fun robust_const_type_args thy (s, T) =
   if s = app_op_name then
     let val (T1, T2) = T |> domain_type |> dest_funT in [T1, T2] end
   else if String.isPrefix old_skolem_const_prefix s then
@@ -573,7 +573,7 @@
     in (IApp (P', Q'), union (op =) P_atomics_Ts Q_atomics_Ts) end
   | iterm_from_term thy type_enc _ (Const (c, T)) =
     (IConst (`(make_fixed_const (SOME type_enc)) c, T,
-             robust_const_typargs thy (c, T)),
+             robust_const_type_args thy (c, T)),
      atomic_types_of T)
   | iterm_from_term _ _ _ (Free (s, T)) =
     (IConst (`make_fixed_var s, T, []), atomic_types_of T)
@@ -870,7 +870,7 @@
                   T
                 else
                   dummyT
-              val U_args = (s, U) |> robust_const_typargs thy
+              val U_args = (s, U) |> robust_const_type_args thy
             in map (filt o apfst dest_TVar) (U_args ~~ T_args) end
             handle TYPE _ => T_args
         val noninfer_type_args = gen_type_args (not o fst) (chop_fun ary)
@@ -1087,11 +1087,14 @@
 
 fun unmangled_const_name s =
   (s, s) |> unaliased_uncurried |> fst |> space_explode mangled_type_sep
+
 fun unmangled_const s =
   let val ss = unmangled_const_name s in
     (hd ss, map unmangled_type (tl ss))
   end
 
+val unmangled_invert_const = invert_const o hd o unmangled_const_name
+
 fun introduce_proxies_in_iterm type_enc =
   let
     fun tweak_ho_quant ho_quant T [IAbs _] = IConst (`I ho_quant, T, [])
@@ -1174,7 +1177,7 @@
       if level_of_type_enc type_enc = No_Types orelse s = tptp_choice then []
       else T_args
     | SOME s'' =>
-      filter_type_args thy constrs type_enc (invert_const s'') ary T_args
+      filter_type_args thy constrs type_enc (unmangled_invert_const s'') ary T_args
 fun filter_type_args_in_iterm thy constrs type_enc =
   let
     fun filt ary (IApp (tm1, tm2)) = IApp (filt (ary + 1) tm1, filt 0 tm2)
@@ -1341,8 +1344,8 @@
   (case unprefix_and_unascii const_prefix s of
      SOME s =>
      let fun tvars_of T = [] |> Term.add_tvarsT T |> map fst in
-       s |> invert_const |> robust_const_type thy |> chop_fun ary |> fst
-         |> map tvars_of
+       s |> unmangled_invert_const |> robust_const_type thy |> chop_fun ary
+         |> fst |> map tvars_of
      end
    | NONE => [])
   handle TYPE _ => []
@@ -1551,8 +1554,7 @@
                         (if String.isSubstring uncurried_alias_sep s then
                            ary
                          else case try (robust_const_ary thy
-                                        o invert_const o hd
-                                        o unmangled_const_name) s of
+                                        o unmangled_invert_const) s of
                            SOME ary0 => Int.min (ary0, ary)
                          | NONE => ary)
                       | NONE => ary
@@ -1595,7 +1597,7 @@
   | NONE =>
     case unprefix_and_unascii const_prefix s of
       SOME s =>
-      let val s = s |> unmangled_const_name |> hd |> invert_const in
+      let val s = s |> unmangled_invert_const in
         if s = predicator_name then 1
         else if s = app_op_name then 2
         else if s = type_guard_name then 1
@@ -1859,7 +1861,7 @@
     fun add (Const (@{const_name Meson.skolem}, _) $ _) = I
       | add (t $ u) = add t #> add u
       | add (Const x) =
-        x |> robust_const_typargs thy |> fold (fold_type_constrs set_insert)
+        x |> robust_const_type_args thy |> fold (fold_type_constrs set_insert)
       | add (Abs (_, _, u)) = add u
       | add _ = I
   in add end
@@ -2387,9 +2389,9 @@
       else case unprefix_and_unascii const_prefix s of
         SOME s' =>
         let
-          val s' = s' |> invert_const
+          val s' = s' |> unmangled_invert_const
           val T = s' |> robust_const_type thy
-        in (T, robust_const_typargs thy (s', T)) end
+        in (T, robust_const_type_args thy (s', T)) end
       | NONE => raise Fail "unexpected type arguments"
   in
     Sym_Decl (sym_decl_prefix ^ s, (s, s'),
@@ -2522,7 +2524,7 @@
         val (role, maybe_negate) = honor_conj_sym_role in_conj
         val base_name = base_s0 |> `(make_fixed_const (SOME type_enc))
         val T = case types of [T] => T | _ => robust_const_type thy base_s0
-        val T_args = robust_const_typargs thy (base_s0, T)
+        val T_args = robust_const_type_args thy (base_s0, T)
         val (base_name as (base_s, _), T_args) =
           mangle_type_args_in_const type_enc base_name T_args
         val base_ary = min_ary_of sym_tab0 base_s
@@ -2564,7 +2566,7 @@
     SOME mangled_s =>
     if String.isSubstring uncurried_alias_sep mangled_s then
       let
-        val base_s0 = mangled_s |> unmangled_const_name |> hd |> invert_const
+        val base_s0 = mangled_s |> unmangled_invert_const
       in
         do_uncurried_alias_lines_for_sym ctxt constrs mono type_enc sym_tab0
                                          sym_tab base_s0 types in_conj min_ary