# HG changeset patch
# User blanchet
# Date 1277743627 -7200
# Node ID b3f572839570d5d789ae39afd80568ce6660da5e
# Parent  3e78dbf7a38259025d010292abdbcac66e040e5b
no setup is necessary anymore

diff -r 3e78dbf7a382 -r b3f572839570 src/HOL/Metis_Examples/Tarski.thy
--- a/src/HOL/Metis_Examples/Tarski.thy	Mon Jun 28 18:46:42 2010 +0200
+++ b/src/HOL/Metis_Examples/Tarski.thy	Mon Jun 28 18:47:07 2010 +0200
@@ -507,9 +507,8 @@
 
 (*never proved, 2007-01-22*)
 declare [[ atp_problem_prefix = "Tarski__CLF_lubH_is_fixp" ]]
-(*Single-step version fails. The conjecture clauses refer to local abstraction
-functions (Frees), which prevents expand_defs_tac from removing those 
-"definitions" at the end of the proof. *)
+(* Single-step version fails. The conjecture clauses refer to local abstraction
+functions (Frees). *)
 lemma (in CLF) lubH_is_fixp:
      "H = {x. (x, f x) \<in> r & x \<in> A} ==> lub H cl \<in> fix f A"
 apply (simp add: fix_def)
diff -r 3e78dbf7a382 -r b3f572839570 src/HOL/Sledgehammer.thy
--- a/src/HOL/Sledgehammer.thy	Mon Jun 28 18:46:42 2010 +0200
+++ b/src/HOL/Sledgehammer.thy	Mon Jun 28 18:47:07 2010 +0200
@@ -86,8 +86,6 @@
 done
 
 use "Tools/Sledgehammer/clausifier.ML"
-setup Clausifier.setup
-
 use "Tools/Sledgehammer/meson_tactic.ML"
 setup Meson_Tactic.setup