# HG changeset patch
# User blanchet
# Date 1310649278 -7200
# Node ID fbc3d9a3a6cd01ecd37001a3e8161dc5e6f782a0
# Parent  0234156d3fbe9c9e96d20f3f8ae1c68567dbd4fc
use monomorphic encoding as fallback, since they tend to produce fewer type errors

diff -r 0234156d3fbe -r fbc3d9a3a6cd src/HOL/Tools/Metis/metis_tactics.ML
--- 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"