| changeset 43825 | fbc3d9a3a6cd |
| parent 43626 | a867ebb12209 |
| child 43963 | 78c723cc3d99 |
--- 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"