# HG changeset patch # User wenzelm # Date 1465325107 -7200 # Node ID 7bd64a07fe43ecbb09a2b04e769341ab8c174262 # Parent d097baa19bd9285ebb6edea388816d03d926704c less ambitious arguments: thms only, no context declaration; diff -r d097baa19bd9 -r 7bd64a07fe43 src/HOL/Eisbach/Eisbach.thy --- 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 = \ - 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) \ \indicate method facts and context for method expression\ end