# HG changeset patch
# User blanchet
# Date 1291735627 -3600
# Node ID 3890ef4e02f9fec9e0d7f3a33ad4a1bb73ce52fa
# Parent  13424972ade4128217ba50c120908af7c5c31b74
pass constant arguments to the built-in check function, cf. d2b1fc1b8e19

diff -r 13424972ade4 -r 3890ef4e02f9 src/HOL/Tools/Sledgehammer/sledgehammer.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Tue Dec 07 15:55:35 2010 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Tue Dec 07 16:27:07 2010 +0100
@@ -53,7 +53,7 @@
   val is_prover_installed : Proof.context -> string -> bool
   val default_max_relevant_for_prover : Proof.context -> string -> int
   val is_built_in_const_for_prover :
-    Proof.context -> string -> string * typ -> bool
+    Proof.context -> string -> string * typ -> term list -> bool
   val relevance_fudge_for_prover : Proof.context -> string -> relevance_fudge
   val dest_dir : string Config.T
   val problem_prefix : string Config.T
@@ -134,8 +134,8 @@
   [@{const_name False}, @{const_name True}, @{const_name If}, @{const_name Let},
    @{const_name HOL.eq}]
 
-fun is_built_in_const_for_prover ctxt name (s, T) =
-  if is_smt_prover ctxt name then SMT_Builtin.is_builtin_ext ctxt (s, T) [] (*FIXME*)
+fun is_built_in_const_for_prover ctxt name (s, T) args =
+  if is_smt_prover ctxt name then SMT_Builtin.is_builtin_ext ctxt (s, T) args
   else member (op =) atp_irrelevant_consts s
 
 (* FUDGE *)
diff -r 13424972ade4 -r 3890ef4e02f9 src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML	Tue Dec 07 15:55:35 2010 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML	Tue Dec 07 16:27:07 2010 +0100
@@ -38,8 +38,9 @@
     Proof.context -> unit Symtab.table -> thm list
     -> Facts.ref * Attrib.src list -> ((string * locality) * thm) list
   val relevant_facts :
-    Proof.context -> bool -> real * real -> int -> (string * typ -> bool)
-    -> relevance_fudge -> relevance_override -> thm list -> term list -> term
+    Proof.context -> bool -> real * real -> int
+    -> (string * typ -> term list -> bool) -> relevance_fudge
+    -> relevance_override -> thm list -> term list -> term
     -> ((string * locality) * thm) list
 end;
 
@@ -182,19 +183,16 @@
 and pconst thy const (s, T) ts = (s, ptype thy const (s, T) ts)
 and rich_ptype thy const (s, T) ts =
   PType (order_of_type T, ptype thy const (s, T) ts)
-and rich_pconst thy const x ts = (x, rich_ptype thy const x ts)
+and rich_pconst thy const (s, T) ts = (s, rich_ptype thy const (s, T) ts)
 
 fun string_for_hyper_pconst (s, ps) =
   s ^ "{" ^ commas (map string_for_ptype ps) ^ "}"
 
 (* Add a pconstant to the table, but a [] entry means a standard
    connective, which we ignore.*)
-fun add_pconst_to_table is_built_in_const also_skolem ((s, T), p) =
-  if is_built_in_const (s, T) orelse
-     (not also_skolem andalso String.isPrefix skolem_prefix s) then
-    I
-  else
-    Symtab.map_default (s, [p]) (insert (op =) p)
+fun add_pconst_to_table also_skolem (s, p) =
+  if (not also_skolem andalso String.isPrefix skolem_prefix s) then I
+  else Symtab.map_default (s, [p]) (insert (op =) p)
 
 fun is_formula_type T = (T = HOLogic.boolT orelse T = propT)
 
@@ -205,8 +203,8 @@
        each quantifiers that must necessarily be skolemized by the ATP, we
        introduce a fresh constant to simulate the effect of Skolemization. *)
     fun do_const const x ts =
-      add_pconst_to_table is_built_in_const also_skolems
-                          (rich_pconst thy const x ts)
+      (not (is_built_in_const x ts)
+       ? add_pconst_to_table also_skolems (rich_pconst thy const x ts))
       #> fold do_term ts
     and do_term t =
       case strip_comb t of
@@ -214,15 +212,14 @@
       | (Free x, ts) => do_const false x ts
       | (Abs (_, T, t'), ts) =>
         (null ts
-         ? add_pconst_to_table (K false) true
-                          ((abs_name, dummyT), PType (order_of_type T + 1, [])))
+         ? add_pconst_to_table true (abs_name, PType (order_of_type T + 1, [])))
         #> fold do_term (t' :: ts)
       | (_, ts) => fold do_term ts
     fun do_quantifier will_surely_be_skolemized abs_T body_t =
       do_formula pos body_t
       #> (if also_skolems andalso will_surely_be_skolemized then
-            add_pconst_to_table (K false) true
-               ((gensym skolem_prefix, dummyT), PType (order_of_type abs_T, []))
+            add_pconst_to_table true
+                (gensym skolem_prefix, PType (order_of_type abs_T, []))
           else
             I)
     and do_term_or_formula T =
@@ -463,8 +460,7 @@
                 take_most_relevant max_relevant remaining_max fudge candidates
               val rel_const_tab' =
                 rel_const_tab
-                |> fold (add_pconst_to_table (K false) false)
-                        (maps (map (apfst (rpair dummyT)) o snd o fst) accepts)
+                |> fold (add_pconst_to_table false) (maps (snd o fst) accepts)
               fun is_dirty (c, _) =
                 Symtab.lookup rel_const_tab' c <> Symtab.lookup rel_const_tab c
               val (hopeful_rejects, hopeless_rejects) =