remove "higher_order" option from Sledgehammer -- the "smart" default is good enough

--- a/src/HOL/Tools/ATP_Manager/atp_manager.ML	Tue Apr 27 10:51:39 2010 +0200
+++ b/src/HOL/Tools/ATP_Manager/atp_manager.ML	Tue Apr 27 11:24:47 2010 +0200
@@ -22,7 +22,6 @@
      relevance_threshold: real,
      convergence: real,
      theory_relevant: bool option,
-     higher_order: bool option,
      follow_defs: bool,
      isar_proof: bool,
      shrink_factor: int,
@@ -83,7 +82,6 @@
    relevance_threshold: real,
    convergence: real,
    theory_relevant: bool option,
-   higher_order: bool option,
    follow_defs: bool,
    isar_proof: bool,
    shrink_factor: int,

--- a/src/HOL/Tools/ATP_Manager/atp_systems.ML	Tue Apr 27 10:51:39 2010 +0200
+++ b/src/HOL/Tools/ATP_Manager/atp_systems.ML	Tue Apr 27 11:24:47 2010 +0200
@@ -233,14 +233,13 @@
         (name, {home, executable, arguments, proof_delims, known_failures,
                 max_axiom_clauses, prefers_theory_relevant})
         (params as {debug, overlord, respect_no_atp, relevance_threshold,
-                    convergence, theory_relevant, higher_order, follow_defs,
-                    isar_proof, ...})
+                    convergence, theory_relevant, follow_defs, isar_proof, ...})
         minimize_command timeout =
   generic_prover overlord
       (get_relevant_facts respect_no_atp relevance_threshold convergence
-                          higher_order follow_defs max_axiom_clauses
+                          follow_defs max_axiom_clauses
                           (the_default prefers_theory_relevant theory_relevant))
-      (prepare_clauses higher_order false)
+      (prepare_clauses false)
       (write_tptp_file (debug andalso overlord)) home
       executable (arguments timeout) proof_delims known_failures name params
       minimize_command
@@ -305,13 +304,13 @@
         (name, {home, executable, arguments, proof_delims, known_failures,
                 max_axiom_clauses, prefers_theory_relevant})
         (params as {overlord, respect_no_atp, relevance_threshold, convergence,
-                    theory_relevant, higher_order, follow_defs, ...})
+                    theory_relevant, follow_defs, ...})
         minimize_command timeout =
   generic_prover overlord
       (get_relevant_facts respect_no_atp relevance_threshold convergence
-                          higher_order follow_defs max_axiom_clauses
+                          follow_defs max_axiom_clauses
                           (the_default prefers_theory_relevant theory_relevant))
-      (prepare_clauses higher_order true) write_dfg_file home executable
+      (prepare_clauses true) write_dfg_file home executable
       (arguments timeout) proof_delims known_failures name params
       minimize_command
 

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML	Tue Apr 27 10:51:39 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML	Tue Apr 27 11:24:47 2010 +0200
@@ -10,6 +10,7 @@
   type axiom_name = Sledgehammer_HOL_Clause.axiom_name
   type hol_clause = Sledgehammer_HOL_Clause.hol_clause
   type hol_clause_id = Sledgehammer_HOL_Clause.hol_clause_id
+
   type relevance_override =
     {add: Facts.ref list,
      del: Facts.ref list,
@@ -19,15 +20,15 @@
   val tfree_classes_of_terms : term list -> string list
   val type_consts_of_terms : theory -> term list -> string list
   val get_relevant_facts :
-    bool -> real -> real -> bool option -> bool -> int -> bool
-    -> relevance_override -> Proof.context * (thm list * 'a) -> thm list
+    bool -> real -> real -> bool -> int -> bool -> relevance_override
+    -> Proof.context * (thm list * 'a) -> thm list
     -> (thm * (string * int)) list
-  val prepare_clauses : bool option -> bool -> thm list -> thm list ->
-    (thm * (axiom_name * hol_clause_id)) list ->
-    (thm * (axiom_name * hol_clause_id)) list -> theory ->
-    axiom_name vector *
-      (hol_clause list * hol_clause list * hol_clause list *
-      hol_clause list * classrel_clause list * arity_clause list)
+  val prepare_clauses :
+    bool -> thm list -> thm list -> (thm * (axiom_name * hol_clause_id)) list
+    -> (thm * (axiom_name * hol_clause_id)) list -> theory
+    -> axiom_name vector
+       * (hol_clause list * hol_clause list * hol_clause list *
+          hol_clause list * classrel_clause list * arity_clause list)
 end;
 
 structure Sledgehammer_Fact_Filter : SLEDGEHAMMER_FACT_FILTER =
@@ -500,13 +501,10 @@
   likely to lead to unsound proofs.*)
 fun remove_unwanted_clauses cls = filter (not o unwanted o prop_of o fst) cls;
 
-fun is_first_order thy higher_order goal_cls =
-  case higher_order of
-    NONE => forall (Meson.is_fol_term thy) (map prop_of goal_cls)
-  | SOME b => not b
+fun is_first_order thy = forall (Meson.is_fol_term thy) o map prop_of
 
 fun get_relevant_facts respect_no_atp relevance_threshold convergence
-                       higher_order follow_defs max_new theory_relevant
+                       follow_defs max_new theory_relevant
                        (relevance_override as {add, only, ...})
                        (ctxt, (chain_ths, th)) goal_cls =
   if (only andalso null add) orelse relevance_threshold > 1.0 then
@@ -514,7 +512,7 @@
   else
     let
       val thy = ProofContext.theory_of ctxt
-      val is_FO = is_first_order thy higher_order goal_cls
+      val is_FO = is_first_order thy goal_cls
       val included_cls = get_all_lemmas respect_no_atp ctxt
         |> cnf_rules_pairs thy |> make_unique
         |> restrict_to_logic thy is_FO
@@ -527,7 +525,7 @@
 
 (* prepare for passing to writer,
    create additional clauses based on the information from extra_cls *)
-fun prepare_clauses higher_order dfg goal_cls chain_ths axcls extra_cls thy =
+fun prepare_clauses dfg goal_cls chain_ths axcls extra_cls thy =
   let
     (* add chain thms *)
     val chain_cls =
@@ -535,7 +533,7 @@
                                   (map (`Thm.get_name_hint) chain_ths))
     val axcls = chain_cls @ axcls
     val extra_cls = chain_cls @ extra_cls
-    val is_FO = is_first_order thy higher_order goal_cls
+    val is_FO = is_first_order thy goal_cls
     val ccls = subtract_cls extra_cls goal_cls
     val _ = app (fn th => trace_msg (fn _ => Display.string_of_thm_global thy th)) ccls
     val ccltms = map prop_of ccls

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Tue Apr 27 10:51:39 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Tue Apr 27 11:24:47 2010 +0200
@@ -96,7 +96,6 @@
    ("relevance_threshold", "50"),
    ("convergence", "320"),
    ("theory_relevant", "smart"),
-   ("higher_order", "smart"),
    ("follow_defs", "false"),
    ("isar_proof", "false"),
    ("shrink_factor", "1"),
@@ -113,14 +112,13 @@
    ("implicit_apply", "explicit_apply"),
    ("ignore_no_atp", "respect_no_atp"),
    ("theory_irrelevant", "theory_relevant"),
-   ("first_order", "higher_order"),
    ("dont_follow_defs", "follow_defs"),
    ("metis_proof", "isar_proof"),
    ("no_sorts", "sorts")]
 
 val params_for_minimize =
   ["debug", "verbose", "overlord", "full_types", "explicit_apply",
-   "higher_order", "isar_proof", "shrink_factor", "sorts", "minimize_timeout"]
+   "isar_proof", "shrink_factor", "sorts", "minimize_timeout"]
 
 val property_dependent_params = ["atps", "full_types", "timeout"]
 
@@ -200,7 +198,6 @@
       0.01 * Real.fromInt (lookup_int "relevance_threshold")
     val convergence = 0.01 * Real.fromInt (lookup_int "convergence")
     val theory_relevant = lookup_bool_option "theory_relevant"
-    val higher_order = lookup_bool_option "higher_order"
     val follow_defs = lookup_bool "follow_defs"
     val isar_proof = lookup_bool "isar_proof"
     val shrink_factor = Int.max (1, lookup_int "shrink_factor")
@@ -212,9 +209,9 @@
      full_types = full_types, explicit_apply = explicit_apply,
      respect_no_atp = respect_no_atp, relevance_threshold = relevance_threshold,
      convergence = convergence, theory_relevant = theory_relevant,
-     higher_order = higher_order, follow_defs = follow_defs,
-     isar_proof = isar_proof, shrink_factor = shrink_factor, sorts = sorts,
-     timeout = timeout, minimize_timeout = minimize_timeout}
+     follow_defs = follow_defs, isar_proof = isar_proof,
+     shrink_factor = shrink_factor, sorts = sorts, timeout = timeout,
+     minimize_timeout = minimize_timeout}
   end
 
 fun get_params thy = extract_params thy (default_raw_params thy)