# HG changeset patch
# User blanchet
# Date 1328019003 -3600
# Node ID ef62c2fafa9e9ecaf7879cbfaf6ac5ebe820c614
# Parent  7e049e9f5c8b7e4dbf00bf6a497b08071eda9072
fixed syntax bug in DFG output

diff -r 7e049e9f5c8b -r ef62c2fafa9e src/HOL/Tools/ATP/atp_problem.ML
--- a/src/HOL/Tools/ATP/atp_problem.ML	Tue Jan 31 14:39:21 2012 +0100
+++ b/src/HOL/Tools/ATP/atp_problem.ML	Tue Jan 31 15:10:03 2012 +0100
@@ -432,6 +432,8 @@
 fun is_predicate_type (AFun (_, ty)) = is_predicate_type ty
   | is_predicate_type (AType (s, _)) = (s = tptp_bool_type)
   | is_predicate_type _ = false
+fun is_nontrivial_predicate_type (AFun (_, ty)) = is_predicate_type ty
+  | is_nontrivial_predicate_type _ = false
 
 fun dfg_string_for_formula flavor info =
   let
@@ -495,7 +497,8 @@
       |> commas |> enclose "functions [" "]."
     val pred_aries =
       filt (fn Decl (_, sym, ty) =>
-               if is_predicate_type ty then SOME (ary sym ty) else NONE
+               if is_nontrivial_predicate_type ty then SOME (ary sym ty)
+               else NONE
              | _ => NONE)
       |> commas |> enclose "predicates [" "]."
     fun sorts () =
diff -r 7e049e9f5c8b -r ef62c2fafa9e src/HOL/Tools/ATP/atp_systems.ML
--- a/src/HOL/Tools/ATP/atp_systems.ML	Tue Jan 31 14:39:21 2012 +0100
+++ b/src/HOL/Tools/ATP/atp_systems.ML	Tue Jan 31 15:10:03 2012 +0100
@@ -360,7 +360,7 @@
    known_failures = #known_failures spass_config,
    conj_sym_kind = #conj_sym_kind spass_config,
    prem_kind = #prem_kind spass_config,
-   best_slices = fn ctxt =>
+   best_slices = fn _ =>
      (* FUDGE *)
      [(0.333, (false, (150, DFG DFG_Sorted, "poly_tags??", combs_and_liftingN,
                        ""))),