1.1 --- a/src/HOL/Tools/Metis/metis_translate.ML	Sun May 01 18:37:25 2011 +0200
     1.2 +++ b/src/HOL/Tools/Metis/metis_translate.ML	Sun May 01 18:37:25 2011 +0200
     1.3 @@ -142,7 +142,7 @@
     1.4    const_trans_table |> Symtab.dest |> map swap |> Symtab.make
     1.5  val const_trans_table_unprox =
     1.6    Symtab.empty
     1.7 -  |> fold (fn (_, (isa, (_, meson))) => Symtab.update (meson, isa))
     1.8 +  |> fold (fn (_, (isa, (_, metis))) => Symtab.update (metis, isa))
     1.9            metis_proxies
    1.10  
    1.11  val invert_const = perhaps (Symtab.lookup const_trans_table_inv)

     2.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML	Sun May 01 18:37:25 2011 +0200
     2.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML	Sun May 01 18:37:25 2011 +0200
     2.3 @@ -106,15 +106,17 @@
     2.4  fun type_system_types_dangerous_types (Tags _) = true
     2.5    | type_system_types_dangerous_types type_sys = is_type_system_sound type_sys
     2.6  
     2.7 -fun dont_need_type_args type_sys s =
     2.8 +val boring_consts = [explicit_app_base, @{const_name Metis.fequal}]
     2.9 +
    2.10 +fun should_omit_type_args type_sys s =
    2.11    s <> type_pred_base andalso
    2.12 -  (member (op =) [@{const_name HOL.eq}] s orelse
    2.13 +  (s = @{const_name HOL.eq} orelse
    2.14     case type_sys of
    2.15       Many_Typed => false
    2.16     | Mangled _ => false
    2.17 -   | Args _ => s = explicit_app_base
    2.18 -   | Tags full_types => full_types orelse s = explicit_app_base
    2.19 -   | No_Types => true)
    2.20 +   | No_Types => true
    2.21 +   | Tags true => true
    2.22 +   | _ => member (op =) boring_consts s)
    2.23  
    2.24  datatype type_arg_policy = No_Type_Args | Mangled_Types | Explicit_Type_Args
    2.25  
    2.26 @@ -123,7 +125,7 @@
    2.27    | general_type_arg_policy _ = Explicit_Type_Args
    2.28  
    2.29  fun type_arg_policy type_sys s =
    2.30 -  if dont_need_type_args type_sys s then No_Type_Args
    2.31 +  if should_omit_type_args type_sys s then No_Type_Args
    2.32    else general_type_arg_policy type_sys
    2.33  
    2.34  fun num_atp_type_args thy type_sys s =