diff -r 5d90d301ad66 -r 54bea620e54f src/HOL/Eisbach/Eisbach_Tools.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Eisbach/Eisbach_Tools.thy	Fri Apr 17 17:49:19 2015 +0200
@@ -0,0 +1,43 @@
+(*  Title:      Eisbach_Tools.thy
+    Author:     Daniel Matichuk, NICTA/UNSW
+
+Usability tools for Eisbach.
+*)
+
+theory Eisbach_Tools
+imports Eisbach
+begin
+
+ML \<open>
+local
+
+fun trace_method parser print =
+  Scan.lift (Args.mode "dummy") -- parser >>
+    (fn (dummy, x) => fn ctxt => SIMPLE_METHOD (fn st =>
+      (if dummy orelse not (Method_Closure.is_dummy st) then tracing (print ctxt x) else ();
+       all_tac st)));
+
+fun setup_trace_method binding parser print =
+  Method.setup binding
+    (trace_method parser (fn ctxt => fn x => Binding.name_of binding ^ ": " ^ print ctxt x))
+    "";
+
+in
+
+val _ =
+  Theory.setup
+   (setup_trace_method @{binding print_fact}
+      (Scan.lift (Scan.ahead Parse.not_eof) -- Attrib.thms)
+      (fn ctxt => fn (tok, thms) =>
+        (* FIXME proper formatting!? *)
+        Token.unparse tok ^ ": " ^ commas (map (Display.string_of_thm ctxt) thms)) #>
+    setup_trace_method @{binding print_term}
+      (Scan.lift (Scan.ahead Parse.not_eof) -- Args.term)
+      (fn ctxt => fn (tok, t) =>
+        (* FIXME proper formatting!? *)
+        Token.unparse tok ^ ": " ^ Syntax.string_of_term ctxt t));
+
+end
+\<close>
+
+end