# HG changeset patch
# User blanchet
# Date 1314346337 -7200
# Node ID 5438d88b2cb7f0af449dd15f423a1be415daa224
# Parent  e08158671ef4b8668cf73dec6cffb0f282e23757
comment

diff -r e08158671ef4 -r 5438d88b2cb7 src/HOL/Tools/ATP/atp_translate.ML
--- a/src/HOL/Tools/ATP/atp_translate.ML	Fri Aug 26 01:18:48 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_translate.ML	Fri Aug 26 10:12:17 2011 +0200
@@ -1253,7 +1253,8 @@
 
 val default_sym_tab_entries : (string * sym_info) list =
   (prefixed_predicator_name,
-   {pred_sym = true, min_ary = 1, max_ary = 1, types = []}) ::
+   {pred_sym = true, min_ary = 1, max_ary = 1, types = []})
+       (* FIXME: needed? *) ::
   (make_fixed_const NONE @{const_name undefined},
    {pred_sym = false, min_ary = 0, max_ary = 0, types = []}) ::
   ([tptp_false, tptp_true]