# HG changeset patch
# User blanchet
# Date 1314309297 -7200
# Node ID c537d5e5a3656bde7b9037de8ebe8aca9ab41269
# Parent  5bde887b47858e0fff2c795f18618f8479448a64
honor TFF Implicit

diff -r 5bde887b4785 -r c537d5e5a365 src/HOL/Tools/ATP/atp_translate.ML
--- a/src/HOL/Tools/ATP/atp_translate.ML	Thu Aug 25 23:38:09 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_translate.ML	Thu Aug 25 23:54:57 2011 +0200
@@ -2176,7 +2176,7 @@
             CNF => ensure_cnf_problem
           | CNF_UEQ => filter_cnf_ueq_problem
           | _ => I)
-      |> (if is_format_typed format then
+      |> (if is_format_typed format andalso format <> TFF Implicit then
             declare_undeclared_syms_in_atp_problem type_decl_prefix
                                                    implicit_declsN
           else