fixed arity of special constants if "explicit_apply" is set

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML	Sun May 01 18:37:24 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML	Sun May 01 18:37:24 2011 +0200
@@ -683,8 +683,13 @@
        String.isPrefix class_prefix s then
       16383 (* large number *)
     else case strip_prefix_and_unascii const_prefix s of
-      SOME s' => s' |> unmangled_const |> fst |> invert_const
-                    |> num_atp_type_args thy type_sys
+      SOME s =>
+      let val s = s |> unmangled_const |> fst |> invert_const in
+        if s = boolify_base then 1
+        else if s = explicit_app_base then 2
+        else if s = type_pred_base then 1
+        else num_atp_type_args thy type_sys s
+      end
     | NONE => 0
 
 (* True if the constant ever appears outside of the top-level position in