# HG changeset patch
# User blanchet
# Date 1314714205 -7200
# Node ID b054ca3f07b57bdc6c665fcee87ffde1e830a3d0
# Parent  03bbadb252db12d7ee12b9c80e42bf443813f56d
"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

diff -r 03bbadb252db -r b054ca3f07b5 src/HOL/Metis_Examples/Type_Encodings.thy
--- 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