# HG changeset patch
# User blanchet
# Date 1314018165 -7200
# Node ID c8b847625584518d528e24f8f89079e86d6b022b
# Parent  e3629929b171708463fa5e66f552f6668e577c0b
include all encodings in tests, now that the incompleteness of some encodings has been addressed

diff -r e3629929b171 -r c8b847625584 src/HOL/Metis_Examples/Type_Encodings.thy
--- 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
@@ -9,7 +9,7 @@
 *}
 
 theory Type_Encodings
-imports "~~/src/HOL/Sledgehammer2d"(*###*)
+imports Main
 begin
 
 declare [[metis_new_skolemizer]]
@@ -22,8 +22,6 @@
 lemma fork: "P \<Longrightarrow> P \<Longrightarrow> P" by assumption
 
 ML {*
-(* The commented-out type systems are too incomplete for our exhaustive
-   tests. *)
 val type_encs =
   ["erased",
    "poly_guards",
@@ -45,7 +43,7 @@
    "poly_guards?",
    "poly_guards_uniform?",
    "poly_tags?",
-(* "poly_tags_uniform?", *)
+   "poly_tags_uniform?",
    "mono_guards?",
    "mono_guards_uniform?",
    "mono_tags?",
@@ -57,7 +55,7 @@
    "simple?",
    "poly_guards!",
    "poly_guards_uniform!",
-(* "poly_tags!", *)
+   "poly_tags!",
    "poly_tags_uniform!",
    "mono_guards!",
    "mono_guards_uniform!",