--- a/src/HOL/Metis_Examples/Type_Encodings.thy Thu Aug 25 14:25:07 2011 +0200
+++ b/src/HOL/Metis_Examples/Type_Encodings.thy Thu Aug 25 14:25:07 2011 +0200
@@ -29,42 +29,42 @@
"poly_tags",
"poly_tags_uniform",
"poly_args",
+ "raw_mono_guards",
+ "raw_mono_guards_uniform",
+ "raw_mono_tags",
+ "raw_mono_tags_uniform",
+ "raw_mono_args",
"mono_guards",
"mono_guards_uniform",
"mono_tags",
"mono_tags_uniform",
"mono_args",
- "mangled_guards",
- "mangled_guards_uniform",
- "mangled_tags",
- "mangled_tags_uniform",
- "mangled_args",
"simple",
"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?",
- "mangled_guards?",
- "mangled_guards_uniform?",
- "mangled_tags?",
- "mangled_tags_uniform?",
"simple?",
"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!",
- "mangled_guards!",
- "mangled_guards_uniform!",
- "mangled_tags!",
- "mangled_tags_uniform!",
"simple!"]
fun metis_exhaust_tac ctxt ths =