# 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