# HG changeset patch
# User blanchet
# Date 1304267845 -7200
# Node ID 0c9a947b43fcf97924011cc189cd8c9a9630093e
# Parent  67e2f2df68d51d2b274d4e76c119ba27b82aeb97
drop "fequal" type args for unmangled type systems

diff -r 67e2f2df68d5 -r 0c9a947b43fc src/HOL/Tools/Metis/metis_translate.ML
--- a/src/HOL/Tools/Metis/metis_translate.ML	Sun May 01 18:37:25 2011 +0200
+++ b/src/HOL/Tools/Metis/metis_translate.ML	Sun May 01 18:37:25 2011 +0200
@@ -142,7 +142,7 @@
   const_trans_table |> Symtab.dest |> map swap |> Symtab.make
 val const_trans_table_unprox =
   Symtab.empty
-  |> fold (fn (_, (isa, (_, meson))) => Symtab.update (meson, isa))
+  |> fold (fn (_, (isa, (_, metis))) => Symtab.update (metis, isa))
           metis_proxies
 
 val invert_const = perhaps (Symtab.lookup const_trans_table_inv)
diff -r 67e2f2df68d5 -r 0c9a947b43fc src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML
--- 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
@@ -106,15 +106,17 @@
 fun type_system_types_dangerous_types (Tags _) = true
   | type_system_types_dangerous_types type_sys = is_type_system_sound type_sys
 
-fun dont_need_type_args type_sys s =
+val boring_consts = [explicit_app_base, @{const_name Metis.fequal}]
+
+fun should_omit_type_args type_sys s =
   s <> type_pred_base andalso
-  (member (op =) [@{const_name HOL.eq}] s orelse
+  (s = @{const_name HOL.eq} orelse
    case type_sys of
      Many_Typed => false
    | Mangled _ => false
-   | Args _ => s = explicit_app_base
-   | Tags full_types => full_types orelse s = explicit_app_base
-   | No_Types => true)
+   | No_Types => true
+   | Tags true => true
+   | _ => member (op =) boring_consts s)
 
 datatype type_arg_policy = No_Type_Args | Mangled_Types | Explicit_Type_Args
 
@@ -123,7 +125,7 @@
   | general_type_arg_policy _ = Explicit_Type_Args
 
 fun type_arg_policy type_sys s =
-  if dont_need_type_args type_sys s then No_Type_Args
+  if should_omit_type_args type_sys s then No_Type_Args
   else general_type_arg_policy type_sys
 
 fun num_atp_type_args thy type_sys s =