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