# HG changeset patch
# User blanchet
# Date 1307385395 -7200
# Node ID 697d32fa183da1bddc1c974fc246cb50b06aad09
# Parent  b16693484c5d927f9aaf7941b32f5ac80e4ebcf8
also exploit type tag idempotence in lightweight encodings, following a suggestion from Gothenburg

diff -r b16693484c5d -r 697d32fa183d src/HOL/Tools/ATP/atp_translate.ML
--- 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