# HG changeset patch
# User wenzelm
# Date 1165683943 -3600
# Node ID 04b4ed5e3033695fae342fd83abf55df7c8579ef
# Parent  88661e47147d4e80dcc5919d7d21f44e084021e9
added term_abbrev;

diff -r 88661e47147d -r 04b4ed5e3033 src/Pure/Isar/args.ML
--- a/src/Pure/Isar/args.ML	Sat Dec 09 18:05:42 2006 +0100
+++ b/src/Pure/Isar/args.ML	Sat Dec 09 18:05:43 2006 +0100
@@ -74,6 +74,7 @@
   val typ_abbrev: Context.generic * T list -> typ * (Context.generic * T list)
   val typ: Context.generic * T list -> typ * (Context.generic * T list)
   val term: Context.generic * T list -> term * (Context.generic * T list)
+  val term_abbrev: Context.generic * T list -> term * (Context.generic * T list)
   val prop: Context.generic * T list -> term * (Context.generic * T list)
   val tyname: Context.generic * T list -> string * (Context.generic * T list)
   val const: Context.generic * T list -> string * (Context.generic * T list)
@@ -318,6 +319,7 @@
 val typ_abbrev = Scan.peek (named_typ o ProofContext.read_typ_abbrev o Context.proof_of);
 val typ = Scan.peek (named_typ o ProofContext.read_typ o Context.proof_of);
 val term = Scan.peek (named_term o ProofContext.read_term o Context.proof_of);
+val term_abbrev = Scan.peek (named_term o ProofContext.read_term_abbrev o Context.proof_of);
 val prop = Scan.peek (named_term o ProofContext.read_prop o Context.proof_of);