# 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 = \<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