# HG changeset patch
# User blanchet
# Date 1304267845 -7200
# Node ID 5737947e4c776127e1ede404a0a3bc563eb68a76
# Parent  7b9801a34836eb9d3f02144e7bb19ec74ff073f5
make sure that fequal keeps its type arguments for mangled type systems

diff -r 7b9801a34836 -r 5737947e4c77 src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML	Sun May 01 18:37:24 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML	Sun May 01 18:37:25 2011 +0200
@@ -233,8 +233,8 @@
                 "c_False" => (tptp_false, s')
               | "c_True" => (tptp_true, s')
               | _ => name, [])
-            else
-              (proxy_base |>> prefix const_prefix, ty_args)
+           else
+             (proxy_base |>> prefix const_prefix, ty_args)
           | NONE => (name, ty_args))
         |> (fn (name, ty_args) => CombConst (name, ty, ty_args))
       | aux _ tm = tm
@@ -477,7 +477,7 @@
         (case strip_prefix_and_unascii const_prefix s of
            NONE => (name, ty_args)
          | SOME s'' =>
-           let val s'' = invert_const s'' in
+           let val s'' = safe_invert_const s'' in
              case type_arg_policy type_sys s'' of
                No_Type_Args => (name, [])
              | Mangled_Types => (mangled_const_name ty_args name, [])
@@ -682,7 +682,7 @@
   | NONE =>
     case strip_prefix_and_unascii const_prefix s of
       SOME s =>
-      let val s = s |> unmangled_const_name |> invert_const in
+      let val s = s |> unmangled_const_name |> safe_invert_const in
         if s = predicator_base then 1
         else if s = explicit_app_base then 2
         else if s = type_pred_base then 1