# HG changeset patch # User blanchet # Date 1306188093 -7200 # Node ID 40bf0173fbedad4961371a238f4335b154ab79e8 # Parent 6e5c2a3c69da902760669ca57d1e71edb5df0c4f pass no type args to hAPP in "poly_args" type system, which is unsound anyway and should correspond as closely as possible to the old unsound encoding diff -r 6e5c2a3c69da -r 40bf0173fbed src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML Mon May 23 19:21:05 2011 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML Tue May 24 00:01:33 2011 +0200 @@ -232,8 +232,13 @@ else Explicit_Type_Args (should_drop_arg_type_args type_sys) -fun type_arg_policy _ @{const_name HOL.eq} = No_Type_Args - | type_arg_policy type_sys _ = general_type_arg_policy type_sys +fun type_arg_policy type_sys s = + if s = @{const_name HOL.eq} orelse + (s = explicit_app_base andalso + level_of_type_sys type_sys = Const_Arg_Types) then + No_Type_Args + else + general_type_arg_policy type_sys fun atp_type_literals_for_types type_sys kind Ts = if level_of_type_sys type_sys = No_Types then