# HG changeset patch
# User blanchet
# Date 1328113015 -3600
# Node ID 8d8d3c1f1854c8bacb33bc05f7d71fcd2e7956a0
# Parent  6467c99c4872d17475536326456d66e9d2a7fca7
really fixed syntax bug in DFG output (cf. ef62c2fafa9e)

diff -r 6467c99c4872 -r 8d8d3c1f1854 src/HOL/Tools/ATP/atp_problem.ML
--- a/src/HOL/Tools/ATP/atp_problem.ML	Wed Feb 01 17:15:06 2012 +0100
+++ b/src/HOL/Tools/ATP/atp_problem.ML	Wed Feb 01 17:16:55 2012 +0100
@@ -497,8 +497,7 @@
       |> commas |> enclose "functions [" "]."
     val pred_aries =
       filt (fn Decl (_, sym, ty) =>
-               if is_nontrivial_predicate_type ty then SOME (ary sym ty)
-               else NONE
+               if is_predicate_type ty then SOME (ary sym ty) else NONE
              | _ => NONE)
       |> commas |> enclose "predicates [" "]."
     fun sorts () =
@@ -513,7 +512,8 @@
              | _ => NONE)
     fun pred_sigs () =
       filt (fn Decl (_, sym, ty) =>
-               if is_predicate_type ty then SOME (pred_typ sym ty) else NONE
+               if is_nontrivial_predicate_type ty then SOME (pred_typ sym ty)
+               else NONE
              | _ => NONE)
     val decls = if sorted then func_sigs () @ pred_sigs () else []
     val axioms = filt (formula (curry (op <>) Conjecture))