1.1 --- a/src/HOL/TPTP/mash_export.ML	Wed Oct 09 10:47:43 2013 +0200
     1.2 +++ b/src/HOL/TPTP/mash_export.ML	Wed Oct 09 15:39:34 2013 +0200
     1.3 @@ -72,7 +72,6 @@
     1.4  
     1.5  fun generate_features ctxt prover thys file_name =
     1.6    let
     1.7 -    val is_built_in_const = Sledgehammer_Provers.is_built_in_const_of_prover ctxt prover
     1.8      val path = file_name |> Path.explode
     1.9      val _ = File.write path ""
    1.10      val facts = all_facts ctxt |> filter_out (has_thys thys o snd)
    1.11 @@ -80,8 +79,7 @@
    1.12        let
    1.13          val name = nickname_of_thm th
    1.14          val feats =
    1.15 -          features_of ctxt is_built_in_const (theory_of_thm th) 0 Symtab.empty stature [prop_of th]
    1.16 -          |> map fst
    1.17 +          features_of ctxt (theory_of_thm th) 0 Symtab.empty stature [prop_of th] |> map fst
    1.18          val s =
    1.19            encode_str name ^ ": " ^ encode_strs (sort string_ord feats) ^ "\n"
    1.20        in File.append path s end
    1.21 @@ -150,7 +148,6 @@
    1.22  fun generate_isar_or_prover_commands ctxt prover params_opt (range, step) thys
    1.23                                       linearize max_suggs file_name =
    1.24    let
    1.25 -    val is_built_in_const = Sledgehammer_Provers.is_built_in_const_of_prover ctxt prover
    1.26      val ho_atp = Sledgehammer_Provers.is_ho_atp ctxt prover
    1.27      val path = file_name |> Path.explode
    1.28      val facts = all_facts ctxt
    1.29 @@ -165,8 +162,7 @@
    1.30            val isar_deps = isar_dependencies_of name_tabs th
    1.31            val do_query = not (is_bad_query ctxt ho_atp step j th isar_deps)
    1.32            val goal_feats =
    1.33 -            features_of ctxt is_built_in_const (theory_of_thm th) (num_old_facts + j) const_tab
    1.34 -              stature [prop_of th]
    1.35 +            features_of ctxt (theory_of_thm th) (num_old_facts + j) const_tab stature [prop_of th]
    1.36              |> sort_wrt fst
    1.37            val access_facts =
    1.38              (if linearize then take (j - 1) new_facts
    1.39 @@ -177,8 +173,7 @@
    1.40            val parents = if linearize then prevs else parents
    1.41            fun extra_features_of (((_, stature), th), weight) =
    1.42              [prop_of th]
    1.43 -            |> features_of ctxt is_built_in_const (theory_of_thm th) (num_old_facts + j) const_tab
    1.44 -              stature
    1.45 +            |> features_of ctxt (theory_of_thm th) (num_old_facts + j) const_tab stature
    1.46              |> map (apsnd (fn r => weight * extra_feature_factor * r))
    1.47            val query =
    1.48              if do_query then

     2.1 --- a/src/HOL/Tools/ATP/atp_problem_generate.ML	Wed Oct 09 10:47:43 2013 +0200
     2.2 +++ b/src/HOL/Tools/ATP/atp_problem_generate.ML	Wed Oct 09 15:39:34 2013 +0200
     2.3 @@ -91,6 +91,8 @@
     2.4    val atp_logical_consts : string list
     2.5    val atp_irrelevant_consts : string list
     2.6    val atp_widely_irrelevant_consts : string list
     2.7 +  val is_irrelevant_const : string -> bool
     2.8 +  val is_widely_irrelevant_const : string -> bool
     2.9    val atp_schematic_consts_of : term -> typ list Symtab.table
    2.10    val is_type_enc_higher_order : type_enc -> bool
    2.11    val is_type_enc_polymorphic : type_enc -> bool
    2.12 @@ -405,19 +407,25 @@
    2.13  (* These are ignored anyway by the relevance filter (unless they appear in
    2.14     higher-order places) but not by the monomorphizer. *)
    2.15  val atp_logical_consts =
    2.16 -  [@{const_name all}, @{const_name "==>"}, @{const_name "=="},
    2.17 -   @{const_name Trueprop}, @{const_name All}, @{const_name Ex},
    2.18 +  [@{const_name prop}, @{const_name Pure.conjunction}, @{const_name all}, @{const_name "==>"},
    2.19 +   @{const_name "=="}, @{const_name Trueprop}, @{const_name All}, @{const_name Ex},
    2.20     @{const_name Ex1}, @{const_name Ball}, @{const_name Bex}]
    2.21  
    2.22  (* These are either simplified away by "Meson.presimplify" (most of the time) or
    2.23     handled specially via "fFalse", "fTrue", ..., "fequal". *)
    2.24  val atp_irrelevant_consts =
    2.25 -  [@{const_name False}, @{const_name True}, @{const_name Not},
    2.26 -   @{const_name conj}, @{const_name disj}, @{const_name implies},
    2.27 -   @{const_name HOL.eq}, @{const_name If}, @{const_name Let}]
    2.28 +  [@{const_name False}, @{const_name True}, @{const_name Not}, @{const_name conj},
    2.29 +   @{const_name disj}, @{const_name implies}, @{const_name HOL.eq}, @{const_name If},
    2.30 +   @{const_name Let}]
    2.31  
    2.32  val atp_widely_irrelevant_consts = atp_logical_consts @ atp_irrelevant_consts
    2.33  
    2.34 +val atp_irrelevant_const_tab = Symtab.make (map (rpair ()) atp_irrelevant_consts)
    2.35 +val atp_widely_irrelevant_const_tab = Symtab.make (map (rpair ()) atp_widely_irrelevant_consts)
    2.36 +
    2.37 +val is_irrelevant_const = Symtab.defined atp_irrelevant_const_tab
    2.38 +val is_widely_irrelevant_const = Symtab.defined atp_widely_irrelevant_const_tab
    2.39 +
    2.40  fun add_schematic_const (x as (_, T)) =
    2.41    Monomorph.typ_has_tvars T ? Symtab.insert_list (op =) x
    2.42  val add_schematic_consts_of =

     3.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Wed Oct 09 10:47:43 2013 +0200
     3.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Wed Oct 09 15:39:34 2013 +0200
     3.3 @@ -63,8 +63,8 @@
     3.4    val run_prover_for_mash :
     3.5      Proof.context -> params -> string -> fact list -> thm -> prover_result
     3.6    val features_of :
     3.7 -    Proof.context -> (string * typ -> term list -> bool * term list) -> theory ->
     3.8 -    int -> int Symtab.table -> stature -> term list -> (string * real) list
     3.9 +    Proof.context -> theory -> int -> int Symtab.table -> stature -> term list ->
    3.10 +    (string * real) list
    3.11    val trim_dependencies : string list -> string list option
    3.12    val isar_dependencies_of :
    3.13      string Symtab.table * string Symtab.table -> thm -> string list
    3.14 @@ -514,20 +514,14 @@
    3.15        val mess = mess |> map (apsnd (apfst (normalize_scores max_facts)))
    3.16        fun score_in fact (global_weight, (sels, unks)) =
    3.17          let
    3.18 -          fun score_at j =
    3.19 -            case try (nth sels) j of
    3.20 -              SOME (_, score) => SOME (global_weight * score)
    3.21 -            | NONE => NONE
    3.22 +          val score_at = try (nth sels) #> Option.map (fn (_, score) => global_weight * score)
    3.23          in
    3.24            case find_index (curry fact_eq fact o fst) sels of
    3.25 -            ~1 => (case find_index (curry fact_eq fact) unks of
    3.26 -                     ~1 => SOME 0.0
    3.27 -                   | _ => NONE)
    3.28 +            ~1 => if member fact_eq unks fact then NONE else SOME 0.0
    3.29            | rank => score_at rank
    3.30          end
    3.31        fun weight_of fact = mess |> map_filter (score_in fact) |> scaled_avg
    3.32 -      val facts =
    3.33 -        fold (union fact_eq o map fst o take max_facts o fst o snd) mess []
    3.34 +      val facts = fold (union fact_eq o map fst o take max_facts o fst o snd) mess []
    3.35      in
    3.36        facts |> map (`weight_of) |> sort (int_ord o swap o pairself fst)
    3.37              |> map snd |> take max_facts
    3.38 @@ -585,9 +579,6 @@
    3.39  
    3.40  val bad_types = [@{type_name prop}, @{type_name bool}, @{type_name fun}]
    3.41  
    3.42 -val logical_consts =
    3.43 -  [@{const_name prop}, @{const_name Pure.conjunction}] @ atp_logical_consts
    3.44 -
    3.45  val pat_tvar_prefix = "_"
    3.46  val pat_var_prefix = "_"
    3.47  
    3.48 @@ -608,15 +599,10 @@
    3.49  
    3.50  val max_pat_breadth = 10 (* FUDGE *)
    3.51  
    3.52 -fun term_features_of ctxt is_built_in_const thy_name num_facts const_tab term_max_depth
    3.53 -                     type_max_depth ts =
    3.54 +fun term_features_of ctxt thy_name num_facts const_tab term_max_depth type_max_depth ts =
    3.55    let
    3.56      val thy = Proof_Context.theory_of ctxt
    3.57  
    3.58 -    fun is_built_in (x as (s, _)) args =
    3.59 -      if member (op =) logical_consts s then (true, args)
    3.60 -      else is_built_in_const x args
    3.61 -
    3.62      val fixes = map snd (Variable.dest_fixes ctxt)
    3.63      val classes = Sign.classes_of thy
    3.64  
    3.65 @@ -660,11 +646,10 @@
    3.66           let val count = Symtab.lookup const_tab s |> the_default 1 in
    3.67             Real.fromInt num_facts / Real.fromInt count (* FUDGE *)
    3.68           end)
    3.69 -    fun pattify_term _ _ 0 _ = []
    3.70 -      | pattify_term _ args _ (Const (x as (s, _))) =
    3.71 -        if fst (is_built_in x args) then []
    3.72 -        else [(massage_long_name s, weight_of_const s)]
    3.73 -      | pattify_term _ _ _ (Free (s, T)) =
    3.74 +    fun pattify_term _ 0 _ = []
    3.75 +      | pattify_term _ _ (Const (s, _)) =
    3.76 +        if is_widely_irrelevant_const s then [] else [(massage_long_name s, weight_of_const s)]
    3.77 +      | pattify_term _ _ (Free (s, T)) =
    3.78          maybe_singleton_str pat_var_prefix (crude_str_of_typ T)
    3.79          |> map (rpair 0.0)
    3.80          |> (if member (op =) fixes s then
    3.81 @@ -672,36 +657,31 @@
    3.82                    (thy_name ^ Long_Name.separator ^ s)))
    3.83              else
    3.84                I)
    3.85 -      | pattify_term _ _ _ (Var (_, T)) =
    3.86 -        maybe_singleton_str pat_var_prefix (crude_str_of_typ T)
    3.87 -        |> map (rpair 0.0)
    3.88 -      | pattify_term Ts _ _ (Bound j) =
    3.89 -        maybe_singleton_str pat_var_prefix (crude_str_of_typ (nth Ts j))
    3.90 -        |> map (rpair 0.0)
    3.91 -      | pattify_term Ts args depth (t $ u) =
    3.92 +      | pattify_term _ _ (Var (_, T)) =
    3.93 +        maybe_singleton_str pat_var_prefix (crude_str_of_typ T) |> map (rpair 0.0)
    3.94 +      | pattify_term Ts _ (Bound j) =
    3.95 +        maybe_singleton_str pat_var_prefix (crude_str_of_typ (nth Ts j)) |> map (rpair 0.0)
    3.96 +      | pattify_term Ts depth (t $ u) =
    3.97          let
    3.98 -          val ps = take max_pat_breadth (pattify_term Ts (u :: args) depth t)
    3.99 -          val qs =
   3.100 -            take max_pat_breadth (("", 0.0) :: pattify_term Ts [] (depth - 1) u)
   3.101 +          val ps = take max_pat_breadth (pattify_term Ts depth t)
   3.102 +          val qs = take max_pat_breadth (("", 0.0) :: pattify_term Ts (depth - 1) u)
   3.103          in
   3.104            map_product (fn ppw as (p, pw) =>
   3.105                fn ("", _) => ppw
   3.106                 | (q, qw) => (p ^ "(" ^ q ^ ")", pw + qw)) ps qs
   3.107          end
   3.108 -      | pattify_term _ _ _ _ = []
   3.109 -    fun add_term_pat Ts = union (eq_fst (op =)) oo pattify_term Ts []
   3.110 +      | pattify_term _ _ _ = []
   3.111 +    fun add_term_pat Ts = union (eq_fst (op =)) oo pattify_term Ts
   3.112      fun add_term_pats _ 0 _ = I
   3.113        | add_term_pats Ts depth t =
   3.114          add_term_pat Ts depth t #> add_term_pats Ts (depth - 1) t
   3.115      fun add_term Ts = add_term_pats Ts term_max_depth
   3.116      fun add_subterms Ts t =
   3.117        case strip_comb t of
   3.118 -        (Const (x as (_, T)), args) =>
   3.119 -        let val (built_in, args) = is_built_in x args in
   3.120 -          (not built_in ? add_term Ts t)
   3.121 -          #> add_subtypes T
   3.122 -          #> fold (add_subterms Ts) args
   3.123 -        end
   3.124 +        (Const (s, T), args) =>
   3.125 +        (not (is_widely_irrelevant_const s) ? add_term Ts t)
   3.126 +        #> add_subtypes T
   3.127 +        #> fold (add_subterms Ts) args
   3.128        | (head, args) =>
   3.129          (case head of
   3.130             Free (_, T) => add_term Ts t #> add_subtypes T
   3.131 @@ -715,11 +695,10 @@
   3.132  val type_max_depth = 1
   3.133  
   3.134  (* TODO: Generate type classes for types? *)
   3.135 -fun features_of ctxt is_built_in_const thy num_facts const_tab (scope, _) ts =
   3.136 +fun features_of ctxt thy num_facts const_tab (scope, _) ts =
   3.137    let val thy_name = Context.theory_name thy in
   3.138      thy_feature_of thy_name ::
   3.139 -    term_features_of ctxt is_built_in_const thy_name num_facts const_tab term_max_depth
   3.140 -      type_max_depth ts
   3.141 +    term_features_of ctxt thy_name num_facts const_tab term_max_depth type_max_depth ts
   3.142      |> scope <> Global ? cons local_feature
   3.143    end
   3.144  
   3.145 @@ -961,7 +940,6 @@
   3.146    let
   3.147      val thy = Proof_Context.theory_of ctxt
   3.148      val thy_name = Context.theory_name thy
   3.149 -    val is_built_in_const = is_built_in_const_of_prover ctxt prover
   3.150      val facts = facts |> sort (crude_thm_ord o pairself snd o swap)
   3.151      val chained = facts |> filter (fn ((_, (scope, _)), _) => scope = Chained)
   3.152      val num_facts = length facts
   3.153 @@ -971,7 +949,7 @@
   3.154        thy_name = Context.theory_name (theory_of_thm th)
   3.155      fun chained_or_extra_features_of factor (((_, stature), th), weight) =
   3.156        [prop_of th]
   3.157 -      |> features_of ctxt is_built_in_const (theory_of_thm th) num_facts const_tab stature
   3.158 +      |> features_of ctxt (theory_of_thm th) num_facts const_tab stature
   3.159        |> map (apsnd (fn r => weight * factor * r))
   3.160  
   3.161      val (access_G, suggs) =
   3.162 @@ -982,8 +960,7 @@
   3.163              let
   3.164                val parents = maximal_wrt_access_graph access_G facts
   3.165                val goal_feats =
   3.166 -                features_of ctxt is_built_in_const thy num_facts const_tab (Local, General)
   3.167 -                  (concl_t :: hyp_ts)
   3.168 +                features_of ctxt thy num_facts const_tab (Local, General) (concl_t :: hyp_ts)
   3.169                val chained_feats =
   3.170                  chained
   3.171                  |> map (rpair 1.0)
   3.172 @@ -1052,10 +1029,7 @@
   3.173          let
   3.174            val thy = Proof_Context.theory_of ctxt
   3.175            val name = freshish_name ()
   3.176 -          val feats =
   3.177 -            features_of ctxt (is_built_in_const_of_prover ctxt prover) thy 0 Symtab.empty
   3.178 -              (Local, General) [t]
   3.179 -            |> map fst
   3.180 +          val feats = features_of ctxt thy 0 Symtab.empty (Local, General) [t] |> map fst
   3.181          in
   3.182            peek_state ctxt overlord (fn {access_G, ...} =>
   3.183                let
   3.184 @@ -1100,7 +1074,6 @@
   3.185          ""
   3.186      else
   3.187        let
   3.188 -        val is_built_in_const = is_built_in_const_of_prover ctxt prover
   3.189          val name_tabs = build_name_tables nickname_of_thm facts
   3.190          fun deps_of status th =
   3.191            if no_dependencies_for_status status then
   3.192 @@ -1155,9 +1128,7 @@
   3.193              let
   3.194                val name = nickname_of_thm th
   3.195                val feats =
   3.196 -                features_of ctxt is_built_in_const (theory_of_thm th) 0 Symtab.empty stature
   3.197 -                  [prop_of th]
   3.198 -                |> map fst
   3.199 +                features_of ctxt (theory_of_thm th) 0 Symtab.empty stature [prop_of th] |> map fst
   3.200                val deps = deps_of status th |> these
   3.201                val n = n |> not (null deps) ? Integer.add 1
   3.202                val learns = (name, parents, feats, deps) :: learns

     4.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_mepo.ML	Wed Oct 09 10:47:43 2013 +0200
     4.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mepo.ML	Wed Oct 09 15:39:34 2013 +0200
     4.3 @@ -58,16 +58,6 @@
     4.4  fun string_of_ptype (PType (_, ps)) = string_of_patternsT ps
     4.5  
     4.6  (*Is the second type an instance of the first one?*)
     4.7 -fun match_pattern (PVar, _) = true
     4.8 -  | match_pattern (_, PVar) = false
     4.9 -  | match_pattern (PApp (s, ps), PApp (t, qs)) =
    4.10 -    s = t andalso match_patterns (ps, qs)
    4.11 -and match_patterns (_, []) = true
    4.12 -  | match_patterns ([], _) = false
    4.13 -  | match_patterns (p :: ps, q :: qs) =
    4.14 -    match_pattern (p, q) andalso match_patterns (ps, qs)
    4.15 -
    4.16 -(*Is the second type an instance of the first one?*)
    4.17  fun match_patternT (TVar _, _) = true
    4.18    | match_patternT (Type (s, ps), Type (t, qs)) =
    4.19      s = t andalso match_patternsT (ps, qs)
    4.20 @@ -116,21 +106,18 @@
    4.21  val set_consts = [@{const_name Collect}, @{const_name Set.member}]
    4.22  val set_thms = @{thms Collect_mem_eq mem_Collect_eq Collect_cong}
    4.23  
    4.24 -fun add_pconsts_in_term thy is_built_in_const =
    4.25 +fun add_pconsts_in_term thy =
    4.26    let
    4.27 -    fun do_const const ext_arg (x as (s, _)) ts =
    4.28 -      let val (built_in, ts) = is_built_in_const x ts in
    4.29 -        if member (op =) set_consts s then
    4.30 -          fold (do_term ext_arg) ts
    4.31 -        else
    4.32 -          (not built_in
    4.33 -           ? add_pconst_to_table (rich_pconst thy const x))
    4.34 -          #> fold (do_term false) ts
    4.35 -      end
    4.36 +    fun do_const const (x as (s, _)) ts =
    4.37 +      if member (op =) set_consts s then
    4.38 +        fold (do_term false) ts
    4.39 +      else
    4.40 +        (not (is_irrelevant_const s) ? add_pconst_to_table (rich_pconst thy const x))
    4.41 +        #> fold (do_term false) ts
    4.42      and do_term ext_arg t =
    4.43        case strip_comb t of
    4.44 -        (Const x, ts) => do_const true ext_arg x ts
    4.45 -      | (Free x, ts) => do_const false ext_arg x ts
    4.46 +        (Const x, ts) => do_const true x ts
    4.47 +      | (Free x, ts) => do_const false x ts
    4.48        | (Abs (_, T, t'), ts) =>
    4.49          ((null ts andalso not ext_arg)
    4.50           (* Since lambdas on the right-hand side of equalities are usually
    4.51 @@ -144,7 +131,7 @@
    4.52        if T = HOLogic.boolT then do_formula else do_term ext_arg
    4.53      and do_formula t =
    4.54        case t of
    4.55 -        Const (@{const_name all}, _) $ Abs (_, T, t') => do_formula t'
    4.56 +        Const (@{const_name all}, _) $ Abs (_, _, t') => do_formula t'
    4.57        | @{const "==>"} $ t1 $ t2 => do_formula t1 #> do_formula t2
    4.58        | Const (@{const_name "=="}, Type (_, [T, _])) $ t1 $ t2 =>
    4.59          do_term_or_formula false T t1 #> do_term_or_formula true T t2
    4.60 @@ -152,8 +139,8 @@
    4.61        | @{const False} => I
    4.62        | @{const True} => I
    4.63        | @{const Not} $ t1 => do_formula t1
    4.64 -      | Const (@{const_name All}, _) $ Abs (_, T, t') => do_formula t'
    4.65 -      | Const (@{const_name Ex}, _) $ Abs (_, T, t') => do_formula t'
    4.66 +      | Const (@{const_name All}, _) $ Abs (_, _, t') => do_formula t'
    4.67 +      | Const (@{const_name Ex}, _) $ Abs (_, _, t') => do_formula t'
    4.68        | @{const HOL.conj} $ t1 $ t2 => do_formula t1 #> do_formula t2
    4.69        | @{const HOL.disj} $ t1 $ t2 => do_formula t1 #> do_formula t2
    4.70        | @{const HOL.implies} $ t1 $ t2 => do_formula t1 #> do_formula t2
    4.71 @@ -162,19 +149,19 @@
    4.72        | Const (@{const_name If}, Type (_, [_, Type (_, [T, _])]))
    4.73          $ t1 $ t2 $ t3 =>
    4.74          do_formula t1 #> fold (do_term_or_formula false T) [t2, t3]
    4.75 -      | Const (@{const_name Ex1}, _) $ Abs (_, T, t') => do_formula t'
    4.76 -      | Const (@{const_name Ball}, _) $ t1 $ Abs (_, T, t') =>
    4.77 +      | Const (@{const_name Ex1}, _) $ Abs (_, _, t') => do_formula t'
    4.78 +      | Const (@{const_name Ball}, _) $ t1 $ Abs (_, _, t') =>
    4.79          do_formula (t1 $ Bound ~1) #> do_formula t'
    4.80 -      | Const (@{const_name Bex}, _) $ t1 $ Abs (_, T, t') =>
    4.81 +      | Const (@{const_name Bex}, _) $ t1 $ Abs (_, _, t') =>
    4.82          do_formula (t1 $ Bound ~1) #> do_formula t'
    4.83        | (t0 as Const (_, @{typ bool})) $ t1 =>
    4.84          do_term false t0 #> do_formula t1  (* theory constant *)
    4.85        | _ => do_term false t
    4.86    in do_formula end
    4.87  
    4.88 -fun pconsts_in_fact thy is_built_in_const t =
    4.89 +fun pconsts_in_fact thy t =
    4.90    Symtab.fold (fn (s, pss) => fold (cons o pair s) pss)
    4.91 -              (Symtab.empty |> add_pconsts_in_term thy is_built_in_const t) []
    4.92 +              (Symtab.empty |> add_pconsts_in_term thy t) []
    4.93  
    4.94  (* Inserts a dummy "constant" referring to the theory name, so that relevance
    4.95     takes the given theory into account. *)
    4.96 @@ -189,9 +176,9 @@
    4.97  fun theory_const_prop_of fudge th =
    4.98    theory_constify fudge (Context.theory_name (theory_of_thm th)) (prop_of th)
    4.99  
   4.100 -fun pair_consts_fact thy is_built_in_const fudge fact =
   4.101 +fun pair_consts_fact thy fudge fact =
   4.102    case fact |> snd |> theory_const_prop_of fudge
   4.103 -            |> pconsts_in_fact thy is_built_in_const of
   4.104 +            |> pconsts_in_fact thy of
   4.105      [] => NONE
   4.106    | consts => SOME ((fact, consts), NONE)
   4.107  
   4.108 @@ -206,13 +193,11 @@
   4.109        EQUAL => dict_ord patternT_ord (ps, qs)
   4.110      | ord => ord)
   4.111    | (TVar _, TVar _) => EQUAL
   4.112 -  | (TVar _, Type _) => LESS
   4.113 -  | (TVar _, TFree _) => LESS
   4.114 +  | (TVar _, _) => LESS
   4.115    | (Type _, TVar _) => GREATER
   4.116 -  | (TFree _, TVar _) => GREATER
   4.117    | (Type _, TFree _) => LESS
   4.118 -  | (TFree _, Type _) => GREATER
   4.119    | (TFree (s, _), TFree (t, _)) => fast_string_ord (s, t)
   4.120 +  | (TFree _, _) => GREATER
   4.121  fun ptype_ord (PType (m, ps), PType (n, qs)) =
   4.122    (case dict_ord patternT_ord (ps, qs) of
   4.123      EQUAL => int_ord (m, n)
   4.124 @@ -357,23 +342,23 @@
   4.125      (accepts, more_rejects @ rejects)
   4.126    end
   4.127  
   4.128 -fun if_empty_replace_with_scope thy is_built_in_const facts sc tab =
   4.129 +fun if_empty_replace_with_scope thy facts sc tab =
   4.130    if Symtab.is_empty tab then
   4.131      Symtab.empty
   4.132 -    |> fold (add_pconsts_in_term thy is_built_in_const)
   4.133 +    |> fold (add_pconsts_in_term thy)
   4.134              (map_filter (fn ((_, (sc', _)), th) =>
   4.135                              if sc' = sc then SOME (prop_of th) else NONE) facts)
   4.136    else
   4.137      tab
   4.138  
   4.139 -fun consider_arities is_built_in_const th =
   4.140 +fun consider_arities th =
   4.141    let
   4.142      fun aux _ _ NONE = NONE
   4.143        | aux t args (SOME tab) =
   4.144          case t of
   4.145            t1 $ t2 => SOME tab |> aux t1 (t2 :: args) |> aux t2 []
   4.146 -        | Const (x as (s, _)) =>
   4.147 -          (if is_built_in_const x args |> fst then
   4.148 +        | Const (s, _) =>
   4.149 +          (if is_widely_irrelevant_const s then
   4.150               SOME tab
   4.151             else case Symtab.lookup tab s of
   4.152               NONE => SOME (Symtab.update (s, length args) tab)
   4.153 @@ -382,9 +367,8 @@
   4.154    in aux (prop_of th) [] end
   4.155  
   4.156  (* FIXME: This is currently only useful for polymorphic type encodings. *)
   4.157 -fun could_benefit_from_ext is_built_in_const facts =
   4.158 -  fold (consider_arities is_built_in_const o snd) facts (SOME Symtab.empty)
   4.159 -  |> is_none
   4.160 +fun could_benefit_from_ext facts =
   4.161 +  fold (consider_arities o snd) facts (SOME Symtab.empty) |> is_none
   4.162  
   4.163  (* High enough so that it isn't wrongly considered as very relevant (e.g., for E
   4.164     weights), but low enough so that it is unlikely to be truncated away if few
   4.165 @@ -395,13 +379,12 @@
   4.166  
   4.167  val really_hopeless_get_kicked_out_iter = 5 (* FUDGE *)
   4.168  
   4.169 -fun relevance_filter ctxt thres0 decay max_facts is_built_in_const
   4.170 -        (fudge as {threshold_divisor, ridiculous_threshold, ...}) facts hyp_ts
   4.171 -        concl_t =
   4.172 +fun relevance_filter ctxt thres0 decay max_facts
   4.173 +        (fudge as {threshold_divisor, ridiculous_threshold, ...}) facts hyp_ts concl_t =
   4.174    let
   4.175      val thy = Proof_Context.theory_of ctxt
   4.176      val const_tab = fold (count_fact_consts thy fudge) facts Symtab.empty
   4.177 -    val add_pconsts = add_pconsts_in_term thy is_built_in_const
   4.178 +    val add_pconsts = add_pconsts_in_term thy
   4.179      val chained_ts =
   4.180        facts |> map_filter (fn ((_, (Chained, _)), th) => SOME (prop_of th)
   4.181                              | _ => NONE)
   4.182 @@ -411,8 +394,7 @@
   4.183        |> fold add_pconsts hyp_ts
   4.184        |> add_pconsts concl_t
   4.185        |> (fn tab => if Symtab.is_empty tab then chained_const_tab else tab)
   4.186 -      |> fold (if_empty_replace_with_scope thy is_built_in_const facts)
   4.187 -              [Chained, Assum, Local]
   4.188 +      |> fold (if_empty_replace_with_scope thy facts) [Chained, Assum, Local]
   4.189      fun iter j remaining_max thres rel_const_tab hopeless hopeful =
   4.190        let
   4.191          val hopeless =
   4.192 @@ -509,11 +491,11 @@
   4.193          in bef @ add @ after end
   4.194      fun insert_special_facts accepts =
   4.195        (* FIXME: get rid of "ext" here once it is treated as a helper *)
   4.196 -      [] |> could_benefit_from_ext is_built_in_const accepts ? cons @{thm ext}
   4.197 +      [] |> could_benefit_from_ext accepts ? cons @{thm ext}
   4.198           |> add_set_const_thms accepts
   4.199           |> insert_into_facts accepts
   4.200    in
   4.201 -    facts |> map_filter (pair_consts_fact thy is_built_in_const fudge)
   4.202 +    facts |> map_filter (pair_consts_fact thy fudge)
   4.203            |> iter 0 max_facts thres0 goal_const_tab []
   4.204            |> insert_special_facts
   4.205            |> tap (fn accepts => trace_msg ctxt (fn () =>
   4.206 @@ -525,8 +507,6 @@
   4.207          max_facts fudge hyp_ts concl_t facts =
   4.208    let
   4.209      val thy = Proof_Context.theory_of ctxt
   4.210 -    val is_built_in_const =
   4.211 -      Sledgehammer_Provers.is_built_in_const_of_prover ctxt prover
   4.212      val fudge =
   4.213        case fudge of
   4.214          SOME fudge => fudge
   4.215 @@ -534,16 +514,14 @@
   4.216      val decay = Math.pow ((1.0 - thres1) / (1.0 - thres0),
   4.217                            1.0 / Real.fromInt (max_facts + 1))
   4.218    in
   4.219 -    trace_msg ctxt (fn () => "Considering " ^ string_of_int (length facts) ^
   4.220 -                             " facts");
   4.221 +    trace_msg ctxt (fn () => "Considering " ^ string_of_int (length facts) ^ " facts");
   4.222      (if thres1 < 0.0 then
   4.223         facts
   4.224       else if thres0 > 1.0 orelse thres0 > thres1 then
   4.225         []
   4.226       else
   4.227 -       relevance_filter ctxt thres0 decay max_facts is_built_in_const fudge
   4.228 -           facts hyp_ts
   4.229 -           (concl_t |> theory_constify fudge (Context.theory_name thy)))
   4.230 +       relevance_filter ctxt thres0 decay max_facts fudge facts hyp_ts
   4.231 +         (concl_t |> theory_constify fudge (Context.theory_name thy)))
   4.232      |> map fact_of_raw_fact
   4.233    end
   4.234  

     5.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Wed Oct 09 10:47:43 2013 +0200
     5.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Wed Oct 09 15:39:34 2013 +0200
     5.3 @@ -120,8 +120,6 @@
     5.4    val default_max_facts_of_prover : Proof.context -> bool -> string -> int
     5.5    val is_unit_equality : term -> bool
     5.6    val is_appropriate_prop_of_prover : Proof.context -> string -> term -> bool
     5.7 -  val is_built_in_const_of_prover :
     5.8 -    Proof.context -> string -> string * typ -> term list -> bool * term list
     5.9    val atp_relevance_fudge : relevance_fudge
    5.10    val smt_relevance_fudge : relevance_fudge
    5.11    val relevance_fudge_of_prover : Proof.context -> string -> relevance_fudge
    5.12 @@ -275,23 +273,6 @@
    5.13  fun is_appropriate_prop_of_prover ctxt name =
    5.14    if is_unit_equational_atp ctxt name then is_unit_equality else K true
    5.15  
    5.16 -val atp_irrelevant_const_tab =
    5.17 -  Symtab.make (map (rpair ()) atp_irrelevant_consts)
    5.18 -
    5.19 -fun is_built_in_const_of_prover ctxt name =
    5.20 -  if is_smt_prover ctxt name andalso Config.get ctxt smt_builtin_facts then
    5.21 -    let val ctxt = ctxt |> select_smt_solver name in
    5.22 -      fn x => fn ts =>
    5.23 -         if SMT_Builtin.is_builtin_num_ext ctxt (list_comb (Const x, ts)) then
    5.24 -           (true, [])
    5.25 -         else if SMT_Builtin.is_builtin_fun_ext ctxt x ts then
    5.26 -           (true, ts)
    5.27 -         else
    5.28 -           (false, ts)
    5.29 -    end
    5.30 -  else
    5.31 -    fn (s, _) => fn ts => (Symtab.defined atp_irrelevant_const_tab s, ts)
    5.32 -
    5.33  (* FUDGE *)
    5.34  val atp_relevance_fudge =
    5.35    {local_const_multiplier = 1.5,
    5.36 @@ -1028,10 +1009,8 @@
    5.37  val is_boring_builtin_typ =
    5.38    not o exists_subtype (member (op =) [@{typ nat}, @{typ int}, HOLogic.realT])
    5.39  
    5.40 -fun smt_filter_loop name
    5.41 -                    ({debug, verbose, overlord, max_mono_iters,
    5.42 -                      max_new_mono_instances, timeout, slice, ...} : params)
    5.43 -                    state goal i =
    5.44 +fun smt_filter_loop name ({debug, overlord, max_mono_iters, max_new_mono_instances, timeout, slice,
    5.45 +      ...} : params) state goal i =
    5.46    let
    5.47      fun repair_context ctxt =
    5.48        ctxt |> select_smt_solver name