src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML
changeset 42570 77f94ac04f32
parent 42569 5737947e4c77
child 42572 0c9a947b43fc
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML	Sun May 01 18:37:25 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML	Sun May 01 18:37:25 2011 +0200
@@ -226,7 +226,7 @@
     fun aux top_level (CombApp (tm1, tm2)) =
         CombApp (aux top_level tm1, aux false tm2)
       | aux top_level (CombConst (name as (s, s'), ty, ty_args)) =
-        (case AList.lookup (op =) metis_proxies s of
+        (case proxify_const s of
            SOME proxy_base =>
            if top_level then
              (case s of
@@ -419,8 +419,7 @@
            t |> (general_type_arg_policy type_sys = Mangled_Types andalso
                  not (null (Term.hidden_polymorphism t)))
                 ? (case typ of
-                     SOME T =>
-                     specialize_type thy (safe_invert_const unmangled_s, T)
+                     SOME T => specialize_type thy (invert_const unmangled_s, T)
                    | NONE => I)
          end)
       fun make_facts eq_as_iff =
@@ -477,7 +476,7 @@
         (case strip_prefix_and_unascii const_prefix s of
            NONE => (name, ty_args)
          | SOME s'' =>
-           let val s'' = safe_invert_const s'' in
+           let val s'' = 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 +681,7 @@
   | NONE =>
     case strip_prefix_and_unascii const_prefix s of
       SOME s =>
-      let val s = s |> unmangled_const_name |> safe_invert_const in
+      let val s = s |> unmangled_const_name |> 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