# HG changeset patch
# User blanchet
# Date 1328353698 -3600
# Node ID 505465fae291bb8750f07663f042582195c286f5
# Parent  8bff5fb211de913e0bd8cd63fc354d5d09c3fd44
tuned SPASS DFG output

diff -r 8bff5fb211de -r 505465fae291 src/HOL/Tools/ATP/atp_problem.ML
--- a/src/HOL/Tools/ATP/atp_problem.ML	Sat Feb 04 12:08:18 2012 +0100
+++ b/src/HOL/Tools/ATP/atp_problem.ML	Sat Feb 04 12:08:18 2012 +0100
@@ -511,35 +511,39 @@
         else
           NONE
       | formula _ _ = NONE
-    fun filt f = problem |> map (map_filter f o snd) |> flat
+    fun filt f = problem |> map (map_filter f o snd) |> filter_out null
     val func_aries =
       filt (fn Decl (_, sym, ty) =>
                if is_function_type ty then SOME (ary sym ty) else NONE
              | _ => NONE)
-      |> commas |> enclose "functions [" "]."
+      |> flat |> commas |> enclose "functions [" "]."
     val pred_aries =
       filt (fn Decl (_, sym, ty) =>
                if is_predicate_type ty then SOME (ary sym ty) else NONE
              | _ => NONE)
-      |> commas |> enclose "predicates [" "]."
+      |> flat |> commas |> enclose "predicates [" "]."
     fun sorts () =
       filt (fn Decl (_, sym, AType (s, [])) =>
                if s = tptp_type_of_types then SOME sym else NONE
-             | _ => NONE) @ [dfg_individual_type]
-      |> commas |> enclose "sorts [" "]."
+             | _ => NONE) @ [[dfg_individual_type]]
+      |> flat |> commas |> enclose "sorts [" "]."
     val syms = [func_aries, pred_aries] @ (if sorted then [sorts ()] else [])
     fun func_sigs () =
       filt (fn Decl (_, sym, ty) =>
                if is_function_type ty then SOME (fun_typ sym ty) else NONE
              | _ => NONE)
+      |> flat
     fun pred_sigs () =
       filt (fn Decl (_, sym, ty) =>
                if is_nontrivial_predicate_type ty then SOME (pred_typ sym ty)
                else NONE
              | _ => NONE)
+      |> flat
     val decls = if sorted then func_sigs () @ pred_sigs () else []
-    val axioms = filt (formula (curry (op <>) Conjecture))
-    val conjs = filt (formula (curry (op =) Conjecture))
+    val axioms =
+      filt (formula (curry (op <>) Conjecture)) |> separate [""] |> flat
+    val conjs =
+      filt (formula (curry (op =) Conjecture)) |> separate [""] |> flat
     fun list_of _ [] = []
       | list_of heading ss =
         "list_of_" ^ heading ^ ".\n" :: map (suffix "\n") ss @