--- a/src/HOL/Metis_Examples/Clausification.thy Thu Jan 03 13:11:04 2013 +0100
+++ b/src/HOL/Metis_Examples/Clausification.thy Thu Jan 03 13:28:37 2013 +0100
@@ -10,10 +10,6 @@
imports Complex_Main
begin
-(* FIXME: shouldn't need this *)
-declare [[unify_search_bound = 100]]
-declare [[unify_trace_bound = 100]]
-
text {* Definitional CNF for facts *}
@@ -139,7 +135,7 @@
lemma
"(\<exists>x \<in> set xs. P x) \<longleftrightarrow>
(\<exists>ys x zs. xs = ys @ x # zs \<and> P x \<and> (\<forall>z \<in> set zs. \<not> P z))"
-by (metis split_list_last_prop [where P = P] in_set_conv_decomp)
+by (metis split_list_last_prop[where P = P] in_set_conv_decomp)
lemma ex_tl: "EX ys. tl ys = xs"
using tl.simps(2) by fast