"simple" was renamed "mono_simple" and there's now "poly_simple" as well -- but they are not needed here since for Metis they amount to the same as guards
--- a/src/HOL/Metis_Examples/Type_Encodings.thy Tue Aug 30 16:11:42 2011 +0200
+++ b/src/HOL/Metis_Examples/Type_Encodings.thy Tue Aug 30 16:23:25 2011 +0200
@@ -39,7 +39,6 @@
"mono_tags",
"mono_tags_uniform",
"mono_args",
- "simple",
"poly_guards?",
"poly_guards_uniform?",
"poly_tags?",
@@ -52,7 +51,6 @@
"mono_guards_uniform?",
"mono_tags?",
"mono_tags_uniform?",
- "simple?",
"poly_guards!",
"poly_guards_uniform!",
"poly_tags!",
@@ -64,8 +62,7 @@
"mono_guards!",
"mono_guards_uniform!",
"mono_tags!",
- "mono_tags_uniform!",
- "simple!"]
+ "mono_tags_uniform!"]
fun metis_exhaust_tac ctxt ths =
let