--- a/src/HOL/Tools/ATP_Manager/atp_manager.ML Tue Jun 22 18:31:49 2010 +0200
+++ b/src/HOL/Tools/ATP_Manager/atp_manager.ML Tue Jun 22 18:47:45 2010 +0200
@@ -67,6 +67,7 @@
open Sledgehammer_Util
open Sledgehammer_Fact_Filter
+open Sledgehammer_HOL_Clause
open Sledgehammer_Proof_Reconstruct
(** problems, results, provers, etc. **)
@@ -355,7 +356,7 @@
filtered_clauses = NONE}
val message =
#message (prover params (minimize_command name) timeout problem)
- handle Sledgehammer_HOL_Clause.TRIVIAL => metis_line full_types i n []
+ handle TRIVIAL () => metis_line full_types i n []
| ERROR message => "Error: " ^ message ^ "\n"
val _ = unregister params message (Thread.self ());
in () end)
--- a/src/HOL/Tools/ATP_Manager/atp_systems.ML Tue Jun 22 18:31:49 2010 +0200
+++ b/src/HOL/Tools/ATP_Manager/atp_systems.ML Tue Jun 22 18:47:45 2010 +0200
@@ -139,10 +139,7 @@
(the_default prefers_theory_relevant theory_relevant)
relevance_override goal goal_cls
| SOME fcls => fcls);
- val the_axiom_clauses =
- (case axiom_clauses of
- NONE => the_filtered_clauses
- | SOME axcls => axcls);
+ val the_axiom_clauses = axiom_clauses |> the_default the_filtered_clauses
val (internal_thm_names, clauses) =
prepare_clauses full_types goal_cls the_axiom_clauses the_filtered_clauses
thy
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML Tue Jun 22 18:31:49 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML Tue Jun 22 18:47:45 2010 +0200
@@ -40,7 +40,7 @@
open Sledgehammer_HOL_Clause
(* Experimental feature: Filter theorems in natural form or in CNF? *)
-val use_natural_form = ref false
+val use_natural_form = Unsynchronized.ref false
type relevance_override =
{add: Facts.ref list,
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_minimizer.ML Tue Jun 22 18:31:49 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_minimizer.ML Tue Jun 22 18:47:45 2010 +0200
@@ -20,6 +20,7 @@
open Sledgehammer_Util
open Sledgehammer_Fact_Preprocessor
+open Sledgehammer_HOL_Clause
open Sledgehammer_Proof_Reconstruct
open ATP_Manager
@@ -125,8 +126,7 @@
\option (e.g., \"timeout = " ^
string_of_int (10 + msecs div 1000) ^ " s\").")
| {message, ...} => (NONE, "ATP error: " ^ message))
- handle Sledgehammer_HOL_Clause.TRIVIAL =>
- (SOME [], metis_line full_types i n [])
+ handle TRIVIAL () => (SOME [], metis_line full_types i n [])
| ERROR msg => (NONE, "Error: " ^ msg)
end
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_hol_clause.ML Tue Jun 22 18:31:49 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_hol_clause.ML Tue Jun 22 18:47:45 2010 +0200
@@ -30,7 +30,7 @@
val literals_of_term : theory -> term -> literal list * typ list
val conceal_skolem_somes :
int -> (string * term) list -> term -> (string * term) list * term
- exception TRIVIAL
+ exception TRIVIAL of unit
val make_conjecture_clauses : theory -> thm list -> hol_clause list
val make_axiom_clauses : theory -> cnf_thm list -> (string * hol_clause) list
val type_wrapper_name : string
@@ -189,7 +189,7 @@
(skolem_somes, t)
(* Trivial problem, which resolution cannot handle (empty clause) *)
-exception TRIVIAL;
+exception TRIVIAL of unit
(* making axiom and conjecture clauses *)
fun make_clause thy (clause_id, axiom_name, kind, th) skolem_somes =
@@ -199,7 +199,7 @@
val (lits, ctypes_sorts) = literals_of_term thy t
in
if forall isFalse lits then
- raise TRIVIAL
+ raise TRIVIAL ()
else
(skolem_somes,
HOLClause {clause_id = clause_id, axiom_name = axiom_name, th = th,