--- a/src/HOL/Eisbach/Tests.thy Tue Jan 05 17:20:56 2016 +0100
+++ b/src/HOL/Eisbach/Tests.thy Tue Jan 05 21:55:34 2016 +0100
@@ -478,6 +478,7 @@
apply (add_my_thms \<open>rule my_thms_named\<close> f:A)
done
+
subsection \<open>Shallow parser tests\<close>
method all_args for A B methods m1 m2 uses f1 f2 declares my_thms_named = fail
@@ -485,6 +486,7 @@
lemma True
by (all_args True False - fail f1: TrueI f2: TrueI my_thms_named: TrueI | rule TrueI)
+
subsection \<open>Method name internalization test\<close>
@@ -494,4 +496,25 @@
lemma "A \<Longrightarrow> A" by test2
+
+subsection \<open>Eisbach method invocation from ML\<close>
+
+method test_method for x y uses r = (print_term x, print_term y, rule r)
+
+method_setup test_method' = \<open>
+ Args.term -- Args.term --
+ (Scan.lift (Args.$$$ "rule" -- Args.colon) |-- Attrib.thms) >>
+ (fn ((x, y), r) => fn ctxt =>
+ Method_Closure.apply_method ctxt "Tests.test_method" [x, y] [r] [] ctxt);
+\<close>
+
+lemma
+ fixes a b :: nat
+ assumes "a = b"
+ shows "b = a"
+ apply (test_method a b)?
+ apply (test_method' a b rule: refl)?
+ apply (test_method' a b rule: assms [symmetric])?
+ done
+
end