src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML
changeset 42951 40bf0173fbed
parent 42944 9e620869a576
child 42956 9aeb0f6ad971
--- 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