# HG changeset patch
# User wenzelm
# Date 1465322382 -7200
# Node ID d097baa19bd9285ebb6edea388816d03d926704c
# Parent  1ee45339e86d2f16e446e1357f6fed42c5c4a93d
added method operator "use";

diff -r 1ee45339e86d -r d097baa19bd9 src/HOL/Eisbach/Eisbach.thy
--- a/src/HOL/Eisbach/Eisbach.thy	Tue Jun 07 19:57:41 2016 +0200
+++ b/src/HOL/Eisbach/Eisbach.thy	Tue Jun 07 19:59:42 2016 +0200
@@ -22,4 +22,20 @@
 
 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)
+\<close> \<open>indicate method facts and context for method expression\<close>
+
 end