--- a/src/HOL/Metis_Examples/Type_Encodings.thy Tue Sep 06 22:41:35 2011 -0700
+++ b/src/HOL/Metis_Examples/Type_Encodings.thy Wed Sep 07 09:10:41 2011 +0200
@@ -25,44 +25,38 @@
val type_encs =
["erased",
"poly_guards",
- "poly_guards_uniform",
+ "poly_guards?",
+ "poly_guards??",
+ "poly_guards!",
+ "poly_guards!!",
"poly_tags",
- "poly_tags_uniform",
+ "poly_tags?",
+ "poly_tags??",
+ "poly_tags!",
+ "poly_tags!!",
"poly_args",
"raw_mono_guards",
- "raw_mono_guards_uniform",
+ "raw_mono_guards?",
+ "raw_mono_guards??",
+ "raw_mono_guards!",
+ "raw_mono_guards!!",
"raw_mono_tags",
- "raw_mono_tags_uniform",
+ "raw_mono_tags?",
+ "raw_mono_tags??",
+ "raw_mono_tags!",
+ "raw_mono_tags!!",
"raw_mono_args",
"mono_guards",
- "mono_guards_uniform",
+ "mono_guards?",
+ "mono_guards??",
+ "mono_guards!",
+ "mono_guards!!",
"mono_tags",
- "mono_tags_uniform",
- "mono_args",
- "poly_guards?",
- "poly_guards_uniform?",
- "poly_tags?",
- "poly_tags_uniform?",
- "raw_mono_guards?",
- "raw_mono_guards_uniform?",
- "raw_mono_tags?",
- "raw_mono_tags_uniform?",
- "mono_guards?",
- "mono_guards_uniform?",
"mono_tags?",
- "mono_tags_uniform?",
- "poly_guards!",
- "poly_guards_uniform!",
- "poly_tags!",
- "poly_tags_uniform!",
- "raw_mono_guards!",
- "raw_mono_guards_uniform!",
- "raw_mono_tags!",
- "raw_mono_tags_uniform!",
- "mono_guards!",
- "mono_guards_uniform!",
+ "mono_tags??",
"mono_tags!",
- "mono_tags_uniform!"]
+ "mono_tags!!",
+ "mono_args"]
fun metis_exhaust_tac ctxt ths =
let