# HG changeset patch
# User wenzelm
# Date 1390821000 -3600
# Node ID a1affe3eb3fd177f8ba9c78e75e0a29583f710e0
# Parent  2733a57d100f5df99856ee2d9d3dc4761f4f67ef
tuned signature;

diff -r 2733a57d100f -r a1affe3eb3fd src/Pure/Isar/args.ML
--- a/src/Pure/Isar/args.ML	Sun Jan 26 16:23:47 2014 +0100
+++ b/src/Pure/Isar/args.ML	Mon Jan 27 12:10:00 2014 +0100
@@ -53,6 +53,7 @@
   val typ_abbrev: typ context_parser
   val typ: typ context_parser
   val term: term context_parser
+  val term_pattern: term context_parser
   val term_abbrev: term context_parser
   val prop: term context_parser
   val type_name: bool -> string context_parser
@@ -198,6 +199,7 @@
 val typ_abbrev = Scan.peek (named_typ o Proof_Context.read_typ_abbrev o Context.proof_of);
 val typ = Scan.peek (named_typ o Syntax.read_typ o Context.proof_of);
 val term = Scan.peek (named_term o Syntax.read_term o Context.proof_of);
+val term_pattern = Scan.peek (named_term o Proof_Context.read_term_pattern o Context.proof_of);
 val term_abbrev = Scan.peek (named_term o Proof_Context.read_term_abbrev o Context.proof_of);
 val prop = Scan.peek (named_term o Syntax.read_prop o Context.proof_of);