# HG changeset patch
# User blanchet
# Date 1323784542 -3600
# Node ID 8f8fce7bd32b544eede1088b61a167bfb7a1673b
# Parent  45a5b6edd4f7b2d11de3b695e644c4dc2b808a11
avoid multiple type decls in TFF (improves on cef82dc1462d)

diff -r 45a5b6edd4f7 -r 8f8fce7bd32b src/HOL/Tools/ATP/atp_translate.ML
--- a/src/HOL/Tools/ATP/atp_translate.ML	Tue Dec 13 14:55:42 2011 +0100
+++ b/src/HOL/Tools/ATP/atp_translate.ML	Tue Dec 13 14:55:42 2011 +0100
@@ -2284,9 +2284,7 @@
 fun problem_lines_for_sym_decls ctxt format conj_sym_kind mono type_enc
                                 (s, decls) =
   case type_enc of
-    Simple_Types _ =>
-    decls |> rationalize_decls ctxt
-          |> map (decl_line_for_sym ctxt format mono type_enc s)
+    Simple_Types _ => [decl_line_for_sym ctxt format mono type_enc s (hd decls)]
   | Guards (_, level) =>
     let
       val decls = decls |> rationalize_decls ctxt