Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
honor TFF Implicit
authorblanchet
Thu, 25 Aug 2011 23:54:57 +0200
changeset 44502 c537d5e5a365
parent 44501 5bde887b4785
child 44503 97ec9abd3253
honor TFF Implicit
src/HOL/Tools/ATP/atp_translate.ML file | annotate | diff | comparison | revisions 
--- 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
isabelle