--- a/src/HOL/Eisbach/Eisbach.thy Wed May 13 19:12:59 2015 +0200
+++ b/src/HOL/Eisbach/Eisbach.thy Sat May 16 12:05:52 2015 +0200
@@ -17,16 +17,16 @@
begin
ML_file "parse_tools.ML"
+ML_file "method_closure.ML"
ML_file "eisbach_rule_insts.ML"
-ML_file "method_closure.ML"
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 true)
+ fold (Method_Closure.wrap_attribute {handle_all_errs = true, declaration = true})
[@{binding intro}, @{binding elim}, @{binding dest}, @{binding simp}] #>
- fold (Method_Closure.wrap_attribute false)
+ fold (Method_Closure.wrap_attribute {handle_all_errs = false, declaration = false})
[@{binding THEN}, @{binding OF}, @{binding rotated}, @{binding simplified}]
\<close>