# HG changeset patch
# User blanchet
# Date 1368632979 -7200
# Node ID 650b7c6b8164f9e883e7cdaa5def132e2957faa8
# Parent  0c04e4c21eb3a8232f498acad9a7dfde64f45a8d
tuned code

diff -r 0c04e4c21eb3 -r 650b7c6b8164 src/HOL/Tools/ATP/atp_problem.ML
--- a/src/HOL/Tools/ATP/atp_problem.ML	Wed May 15 17:49:18 2013 +0200
+++ b/src/HOL/Tools/ATP/atp_problem.ML	Wed May 15 17:49:39 2013 +0200
@@ -622,11 +622,11 @@
              | _ => NONE)
       |> flat |> commas |> maybe_enclose "predicates [" "]."
     val sorts =
-      filt (fn Type_Decl (_, ty, ary) => SOME (ty_ary ary ty) | _ => NONE) @
+      filt (try (fn Type_Decl (_, ty, ary) => ty_ary ary ty)) @
       [[ty_ary 0 dfg_individual_type]]
       |> flat |> commas |> maybe_enclose "sorts [" "]."
     val classes =
-      filt (fn Class_Decl (_, cl, _) => SOME cl | _ => NONE)
+      filt (try (fn Class_Decl (_, cl, _) => cl))
       |> flat |> commas |> maybe_enclose "classes [" "]."
     val ord_info = if gen_weights orelse gen_prec then ord_info () else []
     val do_term_order_weights =
@@ -644,15 +644,14 @@
                else NONE
              | _ => NONE) |> flat
     val datatype_decls =
-      filt (fn Datatype_Decl (_, xs, ty, tms) => SOME (datatype_decl xs ty tms)
-             | _ => NONE) |> flat
+      filt (try (fn Datatype_Decl (_, xs, ty, tms) => datatype_decl xs ty tms))
+      |> flat
     val sort_decls =
-      filt (fn Class_Memb (_, xs, ty, cl) => SOME (sort_decl xs ty cl)
-             | _ => NONE) |> flat
+      filt (try (fn Class_Memb (_, xs, ty, cl) => sort_decl xs ty cl)) |> flat
     val subclass_decls =
-      filt (fn Class_Decl (_, sub, supers) =>
-               SOME (map (subclass_of sub) supers)
-             | _ => NONE) |> flat |> flat
+      filt (try (fn Class_Decl (_, sub, supers) =>
+                    map (subclass_of sub) supers))
+      |> flat |> flat
     val decls =
       func_decls @ pred_decls @ datatype_decls @ sort_decls @ subclass_decls
     val axioms =