--- a/src/HOL/Eisbach/Eisbach.thy Tue Jun 07 19:59:42 2016 +0200
+++ b/src/HOL/Eisbach/Eisbach.thy Tue Jun 07 20:45:07 2016 +0200
@@ -23,19 +23,8 @@
method solves methods m = (m; fail)
method_setup use = \<open>
- Scan.lift (Parse.and_list1 Parse.thms1 --| Parse.$$$ "in") -- Method_Closure.method_text >>
- (fn (raw_args, text) => fn static_ctxt =>
- let
- (* FIXME closure *)
- val args =
- Attrib.map_facts_refs
- (map (Attrib.attribute_cmd static_ctxt)) (Proof_Context.get_fact static_ctxt)
- (map (pair (Binding.empty, [])) raw_args);
- in
- fn _ => fn (ctxt, st) =>
- let val (facts, ctxt') = ctxt |> Proof_Context.note_thmss "" args |>> maps #2
- in Method_Closure.method_evaluate text ctxt' facts (ctxt', st) end
- end)
+ Attrib.thms -- (Scan.lift @{keyword "in"} |-- Method_Closure.method_text) >>
+ (fn (thms, text) => fn ctxt => fn _ => Method_Closure.method_evaluate text ctxt thms)
\<close> \<open>indicate method facts and context for method expression\<close>
end