1.1 --- a/src/Pure/Isar/args.ML	Wed Apr 14 13:25:51 2004 +0200
     1.2 +++ b/src/Pure/Isar/args.ML	Wed Apr 14 13:26:27 2004 +0200
     1.3 @@ -142,23 +142,19 @@
     1.4    Scan.one (fn Arg (k, (x, _)) => k = Keyword andalso OuterLex.is_sid x) >> val_of;
     1.5  
     1.6  fun kind f = Scan.one (K true) :--
     1.7 -  ((fn Arg (Ident, (x, _)) =>
     1.8 +  (fn Arg (Ident, (x, _)) =>
     1.9      (case f x of Some y => Scan.succeed y | _ => Scan.fail)
    1.10 -  | _ => Scan.fail)
    1.11 -(* o (fn (t as Arg (i, (s, _))) =>
    1.12 -  (warning (
    1.13 -    (case i of Ident => "Ident: " | String => "String: "
    1.14 -            | Keyword => "Keyword: " | EOF => "EOF: ")
    1.15 -    ^ s); t)) *) ) >> #2;
    1.16 +  | _ => Scan.fail) >> #2;
    1.17  
    1.18  val nat = kind Syntax.read_nat;
    1.19  val int = Scan.optional ($$$ "-" >> K ~1) 1 -- nat >> op *;
    1.20  
    1.21 -(* Read variable name.  Leading `?' may be omitted if name contains no dot. *)
    1.22 -val var = kind (apsome #1 o
    1.23 -      (fn s => (Some (Term.dest_Var (Syntax.read_var s)))
    1.24 -         handle _ => (Some (Term.dest_Var (Syntax.read_var ("?" ^ s))))
    1.25 -         handle _ => None));
    1.26 +(*read variable name; leading '?' may be omitted if name contains no dot*)
    1.27 +val var = kind (apsome #1 o (fn s =>
    1.28 +  Some (Term.dest_Var (Syntax.read_var s))
    1.29 +    handle _ => Some (Term.dest_Var (Syntax.read_var ("?" ^ s)))
    1.30 +    handle _ => None));
    1.31 +
    1.32  
    1.33  (* enumerations *)
    1.34