# HG changeset patch
# User wenzelm
# Date 911308240 -3600
# Node ID 7da8033264fa2061f8bcd6b1604674fd8b5cac55
# Parent  151ee1a5c09c0841e41e57e31a8e7f164d7ca366
removed trace;

diff -r 151ee1a5c09c -r 7da8033264fa src/Pure/Isar/args.ML
--- a/src/Pure/Isar/args.ML	Tue Nov 17 14:09:29 1998 +0100
+++ b/src/Pure/Isar/args.ML	Tue Nov 17 14:10:40 1998 +0100
@@ -170,16 +170,11 @@
 
 (* argument syntax *)
 
-(* FIXME *)
-fun trace_src kind (Src ((s, args), pos)) =
-  warning ("TRACE: " ^ space_implode " " (kind :: s :: map str_of args) ^ Position.str_of pos);
-
 fun syntax kind scan st (src as Src ((s, args), pos)) =
-  (trace_src kind src;
   (case handle_error (Scan.error (Scan.finite' stopper (Scan.option scan))) (st, args) of
     OK (Some x, (st', [])) => (st', x)
   | OK (_, (_, args')) => err_in_src kind "bad arguments" (Src ((s, args'), pos))
-  | Error msg => err_in_src kind ("\n" ^ msg) src));
+  | Error msg => err_in_src kind ("\n" ^ msg) src);
 
 
 (* attribs *)