# HG changeset patch
# User blanchet
# Date 1292510814 -3600
# Node ID 1e2e16bc007761135d271d352726681f1e7d3a6e
# Parent  15fbf30288e1b631fb75fe7584cc4e3400d188ef
no need to do a super-duper atomization if Metis fails afterwards anyway

diff -r 15fbf30288e1 -r 1e2e16bc0077 src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML	Thu Dec 16 15:44:32 2010 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML	Thu Dec 16 15:46:54 2010 +0100
@@ -226,7 +226,7 @@
     val thy = ProofContext.theory_of ctxt
     val t = t |> Envir.beta_eta_contract
               |> transform_elim_term
-              |> atomize_term
+              |> Object_Logic.atomize_term thy
     val need_trueprop = (fastype_of t = HOLogic.boolT)
     val t = t |> need_trueprop ? HOLogic.mk_Trueprop
               |> extensionalize_term
diff -r 15fbf30288e1 -r 1e2e16bc0077 src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML	Thu Dec 16 15:44:32 2010 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML	Thu Dec 16 15:46:54 2010 +0100
@@ -869,7 +869,7 @@
     val reserved = reserved_isar_keyword_table ()
     val ind_stmt =
       Logic.list_implies (hyp_ts |> filter_out (null o external_frees), concl_t)
-      |> atomize_term
+      |> Object_Logic.atomize_term thy
     val ind_stmt_xs = external_frees ind_stmt
     val facts =
       (if only then
diff -r 15fbf30288e1 -r 1e2e16bc0077 src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Thu Dec 16 15:44:32 2010 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Thu Dec 16 15:46:54 2010 +0100
@@ -487,10 +487,7 @@
             ()
         val birth = Timer.checkRealTimer timer
         val _ =
-          if debug then
-            Output.urgent_message "Invoking SMT solver..."
-          else
-            ()
+          if debug then Output.urgent_message "Invoking SMT solver..." else ()
         val (outcome, used_facts) =
           SMT_Solver.smt_filter remote iter_timeout state facts i
           |> (fn {outcome, used_facts, ...} => (outcome, used_facts))
@@ -525,7 +522,7 @@
                ();
              true (* kind of *))
           | SOME SMT_Failure.Out_Of_Memory => true
-          | SOME _ => true
+          | SOME (SMT_Failure.Other_Failure _) => true
         val timeout = Time.- (timeout, Timer.checkRealTimer timer)
       in
         if too_many_facts_perhaps andalso iter_num < !smt_max_iter andalso
diff -r 15fbf30288e1 -r 1e2e16bc0077 src/HOL/Tools/Sledgehammer/sledgehammer_util.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML	Thu Dec 16 15:44:32 2010 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML	Thu Dec 16 15:46:54 2010 +0100
@@ -16,7 +16,6 @@
   val unyxml : string -> string
   val maybe_quote : string -> string
   val monomorphic_term : Type.tyenv -> term -> term
-  val atomize_term : term -> term
   val eta_expand : typ list -> term -> int -> term
   val transform_elim_term : term -> term
   val specialize_type : theory -> (string * typ) -> term -> term
@@ -88,21 +87,6 @@
       | NONE => raise TERM ("monomorphic_term: uninstanitated schematic type \
                             \variable", [t]))) t
 
-(* "Object_Logic.atomize_term" isn't as powerful as it could be; for example,
-    it leaves metaequalities over "prop"s alone. *)
-val atomize_term =
-  let
-    fun aux (@{const Trueprop} $ t1) = t1
-      | aux (Const (@{const_name all}, _) $ Abs (s, T, t')) =
-        HOLogic.all_const T $ Abs (s, T, aux t')
-      | aux (@{const "==>"} $ t1 $ t2) = HOLogic.mk_imp (pairself aux (t1, t2))
-      | aux (Const (@{const_name "=="}, Type (_, [@{typ prop}, _])) $ t1 $ t2) =
-        HOLogic.eq_const HOLogic.boolT $ aux t1 $ aux t2
-      | aux (Const (@{const_name "=="}, Type (_, [T, _])) $ t1 $ t2) =
-        HOLogic.eq_const T $ t1 $ t2
-      | aux _ = raise Fail "aux"
-  in perhaps (try aux) end
-
 fun eta_expand _ t 0 = t
   | eta_expand Ts (Abs (s, T, t')) n =
     Abs (s, T, eta_expand (T :: Ts) t' (n - 1))