# HG changeset patch
# User blanchet
# Date 1277225265 -7200
# Node ID 32a1ee39c49b2dc6e59853ba1e35084112b7c7de
# Parent  d9af5c01dc4abb71244d1c1a5466783b876c7e78
missing "Unsynchronized" + make exception take a unit

diff -r d9af5c01dc4a -r 32a1ee39c49b src/HOL/Tools/ATP_Manager/atp_manager.ML
--- 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)
diff -r d9af5c01dc4a -r 32a1ee39c49b src/HOL/Tools/ATP_Manager/atp_systems.ML
--- 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
diff -r d9af5c01dc4a -r 32a1ee39c49b src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML
--- 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,
diff -r d9af5c01dc4a -r 32a1ee39c49b src/HOL/Tools/Sledgehammer/sledgehammer_fact_minimizer.ML
--- 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
 
diff -r d9af5c01dc4a -r 32a1ee39c49b src/HOL/Tools/Sledgehammer/sledgehammer_hol_clause.ML
--- 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,