# HG changeset patch
# User blanchet
# Date 1288881086 -3600
# Node ID ff0e17a9d84058cb0cf39794432ba0c2af02e961
# Parent  f16ce22f34d01abc459abc0d3577189cbad0fbf9
pass proper type to SMT_Builtin.is_builtin

diff -r f16ce22f34d0 -r ff0e17a9d840 src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML	Thu Nov 04 15:30:48 2010 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML	Thu Nov 04 15:31:26 2010 +0100
@@ -174,19 +174,19 @@
 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 (s, T) ts = (s, rich_ptype thy const (s, T) ts)
+and rich_pconst thy const x ts = (x, rich_ptype thy const x 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 (c, p) =
-  if is_built_in_const (c, dummyT)(*###*) orelse
-     (not also_skolem andalso String.isPrefix skolem_prefix c) then
+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 (c, [p]) (insert (op =) p)
+    Symtab.map_default (s, [p]) (insert (op =) p)
 
 fun is_formula_type T = (T = HOLogic.boolT orelse T = propT)
 
@@ -196,9 +196,9 @@
     (* We include free variables, as well as constants, to handle locales. For
        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 (s, T) ts =
+    fun do_const const x ts =
       add_pconst_to_table is_built_in_const also_skolems
-                          (rich_pconst thy const (s, T) ts)
+                          (rich_pconst thy const x ts)
       #> fold do_term ts
     and do_term t =
       case strip_comb t of
@@ -206,15 +206,15 @@
       | (Free x, ts) => do_const false x ts
       | (Abs (_, T, t'), ts) =>
         (null ts
-         ? add_pconst_to_table is_built_in_const true
-                               (abs_name, PType (order_of_type T + 1, [])))
+         ? add_pconst_to_table (K false) true
+                          ((abs_name, dummyT), 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 is_built_in_const true
-                         (gensym skolem_prefix, PType (order_of_type abs_T, []))
+            add_pconst_to_table (K false) true
+               ((gensym skolem_prefix, dummyT), PType (order_of_type abs_T, []))
           else
             I)
     and do_term_or_formula T =
@@ -452,8 +452,8 @@
                 take_most_relevant max_relevant remaining_max fudge candidates
               val rel_const_tab' =
                 rel_const_tab
-                |> fold (add_pconst_to_table is_built_in_const false)
-                        (maps (snd o fst) accepts)
+                |> fold (add_pconst_to_table (K false) false)
+                        (maps (map (apfst (rpair dummyT)) o 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) =