--- 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 *)