--- a/src/HOL/Tools/Metis/metis_translate.ML Tue Sep 06 22:41:35 2011 -0700
+++ b/src/HOL/Tools/Metis/metis_translate.ML Wed Sep 07 09:10:41 2011 +0200
@@ -59,7 +59,7 @@
((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, Uniform) => metis_systematic_type_tag
+ (fn Tags (_, All_Types) => metis_systematic_type_tag
| _ => metis_ad_hoc_type_tag, true))]
fun old_skolem_const_name i j num_T_args =