# HG changeset patch
# User blanchet
# Date 1338971705 -7200
# Node ID 60a09522c65eed1476d3d8822fdb325ede6c7c1e
# Parent  bb836e77f590d69e26337a02e9bd75fddce29169
prevent an "Empty" exception (e.g. with Satallax, "mono_native")

diff -r bb836e77f590 -r 60a09522c65e src/HOL/Tools/ATP/atp_problem_generate.ML
--- a/src/HOL/Tools/ATP/atp_problem_generate.ML	Wed Jun 06 10:35:05 2012 +0200
+++ b/src/HOL/Tools/ATP/atp_problem_generate.ML	Wed Jun 06 10:35:05 2012 +0200
@@ -1872,9 +1872,8 @@
         fact :: reorder [] skipped (* break cycle *)
       | reorder skipped (fact :: facts) =
         let val rhs_consts = consts_of_hs snd fact in
-          if exists (exists (member (op =) rhs_consts o the_single
-                     o consts_of_hs fst))
-                    [skipped, facts] then
+          if exists (exists (exists (member (op =) rhs_consts)
+                     o consts_of_hs fst)) [skipped, facts] then
             reorder (fact :: skipped) facts
           else
             fact :: reorder [] (facts @ skipped)
@@ -2649,8 +2648,7 @@
     val lam_trans =
       if lam_trans = keep_lamsN andalso
          not (is_type_enc_higher_order type_enc) then
-        error ("Lambda translation scheme incompatible with first-order \
-               \encoding.")
+        liftingN
       else
         lam_trans
     val (fact_names, classes, conjs, facts, class_rel_clauses, arity_clauses,
@@ -2717,10 +2715,8 @@
     fun add_sym_ary (s, {min_ary, ...} : sym_info) =
       min_ary > 0 ? Symtab.insert (op =) (s, min_ary)
   in
-    (problem,
-     case pool of SOME the_pool => snd the_pool | NONE => Symtab.empty,
-     fact_names |> Vector.fromList,
-     lifted,
+    (problem, pool |> Option.map snd |> the_default Symtab.empty,
+     fact_names |> Vector.fromList, lifted,
      Symtab.empty |> Symtab.fold add_sym_ary sym_tab)
   end