# 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