Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
tuned signature;
authorwenzelm
Mon, 27 Jan 2014 12:10:00 +0100
changeset 55155 a1affe3eb3fd
parent 55154 2733a57d100f
child 55156 3ca79ee6eb33
tuned signature;
src/Pure/Isar/args.ML file | annotate | diff | comparison | revisions 
--- 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);
isabelle