--- a/src/Pure/Isar/args.ML Wed Nov 07 03:51:17 2007 +0100
+++ b/src/Pure/Isar/args.ML Wed Nov 07 16:42:55 2007 +0100
@@ -330,10 +330,10 @@
(* type and constant names *)
-val tyname = Scan.peek (named_typ o Context.cases Sign.read_tyname ProofContext.read_tyname)
+val tyname = Scan.peek (named_typ o ProofContext.read_tyname o Context.proof_of)
>> (fn Type (c, _) => c | TFree (a, _) => a | _ => "");
-val const = Scan.peek (named_term o Context.cases Sign.read_const ProofContext.read_const)
+val const = Scan.peek (named_term o ProofContext.read_const o Context.proof_of)
>> (fn Const (c, _) => c | Free (x, _) => x | _ => "");