# HG changeset patch
# User wenzelm
# Date 1081941987 -7200
# Node ID 4bf2d10461f3ebad180423df86c5d47e74e2f828
# Parent  980da32f46175d873ff7264963f2fc87c72ec7fc
tuned;

diff -r 980da32f4617 -r 4bf2d10461f3 src/Pure/Isar/args.ML
--- a/src/Pure/Isar/args.ML	Wed Apr 14 13:25:51 2004 +0200
+++ b/src/Pure/Isar/args.ML	Wed Apr 14 13:26:27 2004 +0200
@@ -142,23 +142,19 @@
   Scan.one (fn Arg (k, (x, _)) => k = Keyword andalso OuterLex.is_sid x) >> val_of;
 
 fun kind f = Scan.one (K true) :--
-  ((fn Arg (Ident, (x, _)) =>
+  (fn Arg (Ident, (x, _)) =>
     (case f x of Some y => Scan.succeed y | _ => Scan.fail)
-  | _ => Scan.fail)
-(* o (fn (t as Arg (i, (s, _))) =>
-  (warning (
-    (case i of Ident => "Ident: " | String => "String: "
-            | Keyword => "Keyword: " | EOF => "EOF: ")
-    ^ s); t)) *) ) >> #2;
+  | _ => Scan.fail) >> #2;
 
 val nat = kind Syntax.read_nat;
 val int = Scan.optional ($$$ "-" >> K ~1) 1 -- nat >> op *;
 
-(* Read variable name.  Leading `?' may be omitted if name contains no dot. *)
-val var = kind (apsome #1 o
-      (fn s => (Some (Term.dest_Var (Syntax.read_var s)))
-         handle _ => (Some (Term.dest_Var (Syntax.read_var ("?" ^ s))))
-         handle _ => None));
+(*read variable name; leading '?' may be omitted if name contains no dot*)
+val var = kind (apsome #1 o (fn s =>
+  Some (Term.dest_Var (Syntax.read_var s))
+    handle _ => Some (Term.dest_Var (Syntax.read_var ("?" ^ s)))
+    handle _ => None));
+
 
 (* enumerations *)