--- a/src/HOL/Tools/Metis/metis_translate.ML Wed Sep 07 11:36:39 2011 +0200
+++ b/src/HOL/Tools/Metis/metis_translate.ML Wed Sep 07 13:50:16 2011 +0200
@@ -59,8 +59,9 @@
((prefixed_predicator_name, 1), (K metis_predicator, false)),
((prefixed_app_op_name, 2), (K metis_app_op, false)),
((prefixed_type_tag_name, 2),
- (fn Tags (_, All_Types) => metis_systematic_type_tag
- | _ => metis_ad_hoc_type_tag, true))]
+ (fn type_enc =>
+ if level_of_type_enc type_enc = All_Types then metis_systematic_type_tag
+ else metis_ad_hoc_type_tag, true))]
fun old_skolem_const_name i j num_T_args =
old_skolem_const_prefix ^ Long_Name.separator ^