--- 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;