# HG changeset patch
# User blanchet
# Date 1332247989 -3600
# Node ID 3347c853d8e2bd7554af32932bb22f22f5b00347
# Parent  10bece4ac87ea8153ebcbef61737106647f5b5cd
take out experimental polymorphic @ encodings from Metis test -- proof reconstruction is fragile for them

diff -r 10bece4ac87e -r 3347c853d8e2 src/HOL/Metis_Examples/Type_Encodings.thy
--- a/src/HOL/Metis_Examples/Type_Encodings.thy	Tue Mar 20 13:53:09 2012 +0100
+++ b/src/HOL/Metis_Examples/Type_Encodings.thy	Tue Mar 20 13:53:09 2012 +0100
@@ -27,10 +27,10 @@
    "poly_guards",
    "poly_guards?",
    "poly_guards??",
-   "poly_guards@?",
+   (* "poly_guards@?", *)
    "poly_guards!",
    "poly_guards!!",
-   "poly_guards@!",
+   (* "poly_guards@!", *)
    "poly_tags",
    "poly_tags?",
    "poly_tags??",