# HG changeset patch
# User blanchet
# Date 1323270185 -3600
# Node ID cef82dc1462d4b1307b17102faae518422766509
# Parent  eb7b74c7a69b0012e5eb0b19dab9ecfdaea82633
avoid multiple TFF1 declarations

diff -r eb7b74c7a69b -r cef82dc1462d src/HOL/Tools/ATP/atp_translate.ML
--- a/src/HOL/Tools/ATP/atp_translate.ML	Wed Dec 07 16:03:05 2011 +0100
+++ b/src/HOL/Tools/ATP/atp_translate.ML	Wed Dec 07 16:03:05 2011 +0100
@@ -2266,24 +2266,27 @@
 
 fun result_type_of_decl (_, _, T, _, ary, _) = chop_fun ary T |> snd
 
+fun rationalize_decls ctxt (decls as decl :: (decls' as _ :: _)) =
+    let
+      val T = result_type_of_decl decl
+              |> map_type_tvar (fn (z, _) => TVar (z, HOLogic.typeS))
+    in
+      if forall (type_generalization ctxt T o result_type_of_decl) decls' then
+        [decl]
+      else
+        decls
+    end
+  | rationalize_decls _ decls = decls
+
 fun problem_lines_for_sym_decls ctxt format conj_sym_kind mono type_enc
                                 (s, decls) =
   case type_enc of
     Simple_Types _ =>
-    decls |> map (decl_line_for_sym ctxt format mono type_enc s)
+    decls |> rationalize_decls ctxt
+          |> map (decl_line_for_sym ctxt format mono type_enc s)
   | Guards (_, level) =>
     let
-      val decls =
-        case decls of
-          decl :: (decls' as _ :: _) =>
-          let val T = result_type_of_decl decl in
-            if forall (type_generalization ctxt T o result_type_of_decl)
-                      decls' then
-              [decl]
-            else
-              decls
-          end
-        | _ => decls
+      val decls = decls |> rationalize_decls ctxt
       val n = length decls
       val decls =
         decls |> filter (should_encode_type ctxt mono level