# HG changeset patch
# User blanchet
# Date 1304267844 -7200
# Node ID b5eec0c9952874df1c19740c3534eba777d3a06f
# Parent  8591fcc56c34d9d9ef248b0b608555624c338f3f
fixed arity of special constants if "explicit_apply" is set

diff -r 8591fcc56c34 -r b5eec0c99528 src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML
--- 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