1.1 --- a/src/Pure/Isar/args.ML	Wed Nov 07 03:51:17 2007 +0100
     1.2 +++ b/src/Pure/Isar/args.ML	Wed Nov 07 16:42:55 2007 +0100
     1.3 @@ -330,10 +330,10 @@
     1.4  
     1.5  (* type and constant names *)
     1.6  
     1.7 -val tyname = Scan.peek (named_typ o Context.cases Sign.read_tyname ProofContext.read_tyname)
     1.8 +val tyname = Scan.peek (named_typ o ProofContext.read_tyname o Context.proof_of)
     1.9    >> (fn Type (c, _) => c | TFree (a, _) => a | _ => "");
    1.10  
    1.11 -val const = Scan.peek (named_term o Context.cases Sign.read_const ProofContext.read_const)
    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