--- a/src/HOL/Metis_Examples/Type_Encodings.thy Wed Dec 21 15:04:28 2011 +0100
+++ b/src/HOL/Metis_Examples/Type_Encodings.thy Wed Dec 21 18:23:08 2011 +0100
@@ -33,10 +33,8 @@
"poly_tags",
"poly_tags?",
"poly_tags??",
- "poly_tags@?",
"poly_tags!",
"poly_tags!!",
- "poly_tags@!",
"poly_args",
"raw_mono_guards",
"raw_mono_guards?",
@@ -48,10 +46,8 @@
"raw_mono_tags",
"raw_mono_tags?",
"raw_mono_tags??",
- "raw_mono_tags@?",
"raw_mono_tags!",
"raw_mono_tags!!",
- "raw_mono_tags@!",
"raw_mono_args",
"mono_guards",
"mono_guards?",