1.1 --- a/src/Pure/Isar/args.ML	Thu Nov 08 13:24:03 2007 +0100
     1.2 +++ b/src/Pure/Isar/args.ML	Thu Nov 08 14:51:28 2007 +0100
     1.3 @@ -81,6 +81,7 @@
     1.4    val prop: Context.generic * T list -> term * (Context.generic * T list)
     1.5    val tyname: Context.generic * T list -> string * (Context.generic * T list)
     1.6    val const: Context.generic * T list -> string * (Context.generic * T list)
     1.7 +  val const_proper: Context.generic * T list -> string * (Context.generic * T list)
     1.8    val thm_sel: T list -> PureThy.interval list * T list
     1.9    val bang_facts: Context.generic * T list -> thm list * (Context.generic * T list)
    1.10    val goal_spec: ((int -> tactic) -> tactic) -> ('a * T list)
    1.11 @@ -336,6 +337,9 @@
    1.12  val const = Scan.peek (named_term o ProofContext.read_const o Context.proof_of)
    1.13    >> (fn Const (c, _) => c | Free (x, _) => x | _ => "");
    1.14  
    1.15 +val const_proper = Scan.peek (named_term o ProofContext.read_const_proper o Context.proof_of)
    1.16 +  >> (fn Const (c, _) => c | _ => "");
    1.17 +
    1.18  
    1.19  (* misc *)
    1.20