--- a/src/HOL/Metis_Examples/Type_Encodings.thy Mon Aug 22 15:02:45 2011 +0200
+++ b/src/HOL/Metis_Examples/Type_Encodings.thy Mon Aug 22 15:02:45 2011 +0200
@@ -27,46 +27,46 @@
val type_encs =
["erased",
"poly_guards",
- "poly_guards_heavy",
+ "poly_guards_uniform",
"poly_tags",
- "poly_tags_heavy",
+ "poly_tags_uniform",
"poly_args",
"mono_guards",
- "mono_guards_heavy",
+ "mono_guards_uniform",
"mono_tags",
- "mono_tags_heavy",
+ "mono_tags_uniform",
"mono_args",
"mangled_guards",
- "mangled_guards_heavy",
+ "mangled_guards_uniform",
"mangled_tags",
- "mangled_tags_heavy",
+ "mangled_tags_uniform",
"mangled_args",
"simple",
"poly_guards?",
- "poly_guards_heavy?",
+ "poly_guards_uniform?",
"poly_tags?",
-(* "poly_tags_heavy?", *)
+(* "poly_tags_uniform?", *)
"mono_guards?",
- "mono_guards_heavy?",
+ "mono_guards_uniform?",
"mono_tags?",
- "mono_tags_heavy?",
+ "mono_tags_uniform?",
"mangled_guards?",
- "mangled_guards_heavy?",
+ "mangled_guards_uniform?",
"mangled_tags?",
- "mangled_tags_heavy?",
+ "mangled_tags_uniform?",
"simple?",
"poly_guards!",
- "poly_guards_heavy!",
+ "poly_guards_uniform!",
(* "poly_tags!", *)
- "poly_tags_heavy!",
+ "poly_tags_uniform!",
"mono_guards!",
- "mono_guards_heavy!",
+ "mono_guards_uniform!",
"mono_tags!",
- "mono_tags_heavy!",
+ "mono_tags_uniform!",
"mangled_guards!",
- "mangled_guards_heavy!",
+ "mangled_guards_uniform!",
"mangled_tags!",
- "mangled_tags_heavy!",
+ "mangled_tags_uniform!",
"simple!"]
fun metis_exhaust_tac ctxt ths =