also exploit type tag idempotence in lightweight encodings, following a suggestion from Gothenburg

--- a/src/HOL/Tools/ATP/atp_translate.ML	Mon Jun 06 20:36:35 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_translate.ML	Mon Jun 06 20:36:35 2011 +0200
@@ -1791,8 +1791,10 @@
   |-> fold_rev (append o problem_lines_for_sym_decls ctxt format conj_sym_kind
                                                      nonmono_Ts type_sys)
 
-fun needs_type_tag_idempotence (Tags (Polymorphic, level, Heavyweight)) =
-    level = Nonmonotonic_Types orelse level = Finite_Types
+fun needs_type_tag_idempotence (Tags (poly, level, heaviness)) =
+    poly <> Mangled_Monomorphic andalso
+    ((level = All_Types andalso heaviness = Lightweight) orelse
+     level = Nonmonotonic_Types orelse level = Finite_Types)
   | needs_type_tag_idempotence _ = false
 
 fun offset_of_heading_in_problem _ [] j = j