--- a/src/HOL/Eisbach/Eisbach.thy Tue Dec 15 16:57:10 2015 +0100
+++ b/src/HOL/Eisbach/Eisbach.thy Wed Dec 16 16:31:36 2015 +0100
@@ -21,14 +21,6 @@
ML_file "match_method.ML"
ML_file "eisbach_antiquotations.ML"
-(* FIXME reform Isabelle/Pure attributes to make this work by default *)
-setup \<open>
- fold (Method_Closure.wrap_attribute {handle_all_errs = true, declaration = true})
- [@{binding intro}, @{binding elim}, @{binding dest}, @{binding simp}] #>
- fold (Method_Closure.wrap_attribute {handle_all_errs = false, declaration = false})
- [@{binding THEN}, @{binding OF}, @{binding rotated}, @{binding simplified}]
-\<close>
-
method solves methods m = (m; fail)
end