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.
use monomorphic encoding as fallback, since they tend to produce fewer type errors
authorblanchet
Thu, 14 Jul 2011 15:14:38 +0200
changeset 43825 fbc3d9a3a6cd
parent 43824 0234156d3fbe
child 43826 2b094d17f432
use monomorphic encoding as fallback, since they tend to produce fewer type errors
src/HOL/Tools/Metis/metis_tactics.ML file | annotate | diff | comparison | revisions 
--- a/src/HOL/Tools/Metis/metis_tactics.ML	Thu Jul 14 15:14:38 2011 +0200
+++ b/src/HOL/Tools/Metis/metis_tactics.ML	Thu Jul 14 15:14:38 2011 +0200
@@ -39,7 +39,7 @@
 val partial_typesN = "partial_types"
 val no_typesN = "no_types"
 
-val really_full_type_enc = "poly_tags_heavy"
+val really_full_type_enc = "mangled_tags_heavy"
 val full_type_enc = "poly_preds_heavy_query"
 val partial_type_enc = "poly_args"
 val no_type_enc = "erased"
isabelle