Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
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, 25 Aug 2011 14:25:07 +0200
changeset 44493 c2602c5d4b0a
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 file | annotate | diff | comparison | revisions 
--- 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))
isabelle