--- a/src/Pure/Isar/args.ML Thu Feb 25 22:05:34 2010 +0100
+++ b/src/Pure/Isar/args.ML Thu Feb 25 22:06:43 2010 +0100
@@ -54,7 +54,7 @@
val term: term context_parser
val term_abbrev: term context_parser
val prop: term context_parser
- val tyname: string context_parser
+ val type_name: bool -> string context_parser
val const: string context_parser
val const_proper: string context_parser
val bang_facts: thm list context_parser
@@ -209,7 +209,8 @@
(* type and constant names *)
-val tyname = Scan.peek (named_typ o ProofContext.read_tyname o Context.proof_of)
+fun type_name strict =
+ Scan.peek (fn ctxt => named_typ (ProofContext.read_type_name (Context.proof_of ctxt) strict))
>> (fn Type (c, _) => c | TFree (a, _) => a | _ => "");
val const = Scan.peek (named_term o ProofContext.read_const o Context.proof_of)