--- a/src/HOL/Metis_Examples/Proxies.thy Fri Jul 01 15:53:38 2011 +0200
+++ b/src/HOL/Metis_Examples/Proxies.thy Fri Jul 01 15:53:38 2011 +0200
@@ -50,7 +50,7 @@
by linarith
lemma "B \<subseteq> C"
-sledgehammer [type_enc = poly_args, max_relevant = 200, expect = some]
+sledgehammer [type_enc = poly_args, max_relevant = 100, expect = some]
by (metis_exhaust B_def C_def int_le_0_imp_le_1 predicate1I)
--- a/src/HOL/Metis_Examples/Type_Encodings.thy Fri Jul 01 15:53:38 2011 +0200
+++ b/src/HOL/Metis_Examples/Type_Encodings.thy Fri Jul 01 15:53:38 2011 +0200
@@ -43,8 +43,8 @@
"mangled_args",
"simple",
"poly_preds?",
-(* "poly_preds_heavy?", *)
-(* "poly_tags?", *)
+ "poly_preds_heavy?",
+ "poly_tags?",
(* "poly_tags_heavy?", *)
"mono_preds?",
"mono_preds_heavy?",
@@ -56,9 +56,9 @@
"mangled_tags_heavy?",
"simple?",
"poly_preds!",
-(* "poly_preds_heavy!", *)
+ "poly_preds_heavy!",
(* "poly_tags!", *)
-(* "poly_tags_heavy!", *)
+ "poly_tags_heavy!",
"mono_preds!",
"mono_preds_heavy!",
"mono_tags!",