# HG changeset patch
# User wenzelm
# Date 1194529888 -3600
# Node ID 31c55418de5ac456a90e4bd32d665853af4928d4
# Parent  68577e621ea87c4076d62bc18eeb9f48feb623c5
added const_proper;

diff -r 68577e621ea8 -r 31c55418de5a src/Pure/Isar/args.ML
--- a/src/Pure/Isar/args.ML	Thu Nov 08 13:24:03 2007 +0100
+++ b/src/Pure/Isar/args.ML	Thu Nov 08 14:51:28 2007 +0100
@@ -81,6 +81,7 @@
   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)
+  val const_proper: Context.generic * T list -> string * (Context.generic * T list)
   val thm_sel: T list -> PureThy.interval list * T list
   val bang_facts: Context.generic * T list -> thm list * (Context.generic * T list)
   val goal_spec: ((int -> tactic) -> tactic) -> ('a * T list)
@@ -336,6 +337,9 @@
 val const = Scan.peek (named_term o ProofContext.read_const o Context.proof_of)
   >> (fn Const (c, _) => c | Free (x, _) => x | _ => "");
 
+val const_proper = Scan.peek (named_term o ProofContext.read_const_proper o Context.proof_of)
+  >> (fn Const (c, _) => c | _ => "");
+
 
 (* misc *)