handle nonmangled monomorphich the same way as mangled monomorphic when it comes to helper -- otherwise we can end up generating too tight type guards
authorblanchet
Thu Aug 25 14:25:07 2011 +0200 (2011-08-25)
changeset 44493c2602c5d4b0a
parent 44492 a330c0608da8
child 44494 a77901b3774e
handle nonmangled monomorphich the same way as mangled monomorphic when it comes to helper -- otherwise we can end up generating too tight type guards
src/HOL/Tools/ATP/atp_translate.ML
     1.1 --- a/src/HOL/Tools/ATP/atp_translate.ML	Thu Aug 25 14:25:07 2011 +0200
     1.2 +++ b/src/HOL/Tools/ATP/atp_translate.ML	Thu Aug 25 14:25:07 2011 +0200
     1.3 @@ -1447,7 +1447,7 @@
     1.4    end
     1.5  
     1.6  fun should_specialize_helper type_enc t =
     1.7 -  polymorphism_of_type_enc type_enc = Mangled_Monomorphic andalso
     1.8 +  polymorphism_of_type_enc type_enc <> Polymorphic andalso
     1.9    level_of_type_enc type_enc <> No_Types andalso
    1.10    not (null (Term.hidden_polymorphism t))
    1.11