# HG changeset patch
# User blanchet
# Date 1314275107 -7200
# Node ID c2602c5d4b0a756f26f24cdab5f7114aee068d9e
# Parent  a330c0608da82c1e59c6d9a1a7997b3e122c60bf
handle nonmangled monomorphich the same way as mangled monomorphic when it comes to helper -- otherwise we can end up generating too tight type guards

diff -r a330c0608da8 -r c2602c5d4b0a src/HOL/Tools/ATP/atp_translate.ML
--- a/src/HOL/Tools/ATP/atp_translate.ML	Thu Aug 25 14:25:07 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_translate.ML	Thu Aug 25 14:25:07 2011 +0200
@@ -1447,7 +1447,7 @@
   end
 
 fun should_specialize_helper type_enc t =
-  polymorphism_of_type_enc type_enc = Mangled_Monomorphic andalso
+  polymorphism_of_type_enc type_enc <> Polymorphic andalso
   level_of_type_enc type_enc <> No_Types andalso
   not (null (Term.hidden_polymorphism t))