# HG changeset patch
# User blanchet
# Date 1307385395 -7200
# Node ID acfc370df64b06d0fd61e5cb00825db5f657aee1
# Parent  cb8b9786ffe3339d3ef46ab7b0f6feb6bd9a278b
compile

diff -r cb8b9786ffe3 -r acfc370df64b src/HOL/Metis_Examples/Type_Encodings.thy
--- a/src/HOL/Metis_Examples/Type_Encodings.thy	Mon Jun 06 20:36:35 2011 +0200
+++ b/src/HOL/Metis_Examples/Type_Encodings.thy	Mon Jun 06 20:36:35 2011 +0200
@@ -22,23 +22,52 @@
 lemma fork: "P \<Longrightarrow> P \<Longrightarrow> P" by assumption
 
 ML {*
-open ATP_Translate
-
-val polymorphisms = [Polymorphic, Monomorphic, Mangled_Monomorphic]
-val levels =
-  [All_Types, Nonmonotonic_Types, Finite_Types, Const_Arg_Types, No_Types]
-val heaviness = [Heavyweight, Lightweight]
+(* The commented-out type systems are too incomplete for our exhaustive
+   tests. *)
 val type_syss =
-  (levels |> map Simple_Types) @
-  (map_product pair levels heaviness
-   (* The following two families of type systems are too incomplete for our
-      tests. *)
-   |> remove (op =) (Nonmonotonic_Types, Heavyweight)
-   |> remove (op =) (Finite_Types, Heavyweight)
-   |> map_product pair polymorphisms
-   |> map_product (fn constr => fn (poly, (level, heaviness)) =>
-                      constr (poly, level, heaviness))
-                  [Preds, Tags])
+  ["erased",
+   "poly_preds",
+   "poly_preds_heavy",
+   "poly_tags",
+   "poly_tags_heavy",
+   "poly_args",
+   "mono_preds",
+   "mono_preds_heavy",
+   "mono_tags",
+   "mono_tags_heavy",
+   "mono_args",
+   "mangled_preds",
+   "mangled_preds_heavy",
+   "mangled_tags",
+   "mangled_tags_heavy",
+   "mangled_args",
+   "simple",
+   "poly_preds?",
+(* "poly_preds_heavy?", *)
+(* "poly_tags?", *)
+(* "poly_tags_heavy?", *)
+   "mono_preds?",
+   "mono_preds_heavy?",
+   "mono_tags?",
+   "mono_tags_heavy?",
+   "mangled_preds?",
+   "mangled_preds_heavy?",
+   "mangled_tags?",
+   "mangled_tags_heavy?",
+   "simple?",
+   "poly_preds!",
+(* "poly_preds_heavy!", *)
+(* "poly_tags!", *)
+(* "poly_tags_heavy!", *)
+   "mono_preds!",
+   "mono_preds_heavy!",
+   "mono_tags!",
+   "mono_tags_heavy!",
+   "mangled_preds!",
+   "mangled_preds_heavy!",
+   "mangled_tags!",
+   "mangled_tags_heavy!",
+   "simple!"]
 
 fun new_metis_exhaust_tac ctxt ths =
   let