diff -r dd6cd88cebd9 -r 08369e33c185 src/HOL/Eisbach/parse_tools.ML
--- a/src/HOL/Eisbach/parse_tools.ML	Mon May 30 20:58:54 2016 +0200
+++ b/src/HOL/Eisbach/parse_tools.ML	Mon May 30 16:11:53 2016 +1000
@@ -20,6 +20,8 @@
 
   val parse_term_val : 'b parser -> (term, 'b) parse_val parser
   val name_term : (term, string) parse_val parser
+
+  val parse_thm_val : 'b parser -> (thm, 'b) parse_val parser
 end;
 
 structure Parse_Tools: PARSE_TOOLS =
@@ -36,6 +38,11 @@
 
 val name_term = parse_term_val Args.embedded_inner_syntax;
 
+fun parse_thm_val scan =
+  Scan.ahead Parse.not_eof -- Scan.ahead (Scan.option (Args.internal_fact >> the_single)) -- scan >>
+    (fn ((_, SOME t), _) => Real_Val t
+      | ((tok, NONE), v) => Parse_Val (v, fn t => ignore (Token.assign (SOME (Token.Fact (NONE, [t]))) tok)));
+
 fun is_real_val (Real_Val _) = true
   | is_real_val _ = false;