# HG changeset patch
# User wenzelm
# Date 911382998 -3600
# Node ID 50005d6ba6093af32656f1aa9b07df16185d3358
# Parent  d7e35f45b72ceeb973936cc256ecc12fc5fb6d85
removed trace;

diff -r d7e35f45b72c -r 50005d6ba609 src/Pure/Isar/method.ML
--- a/src/Pure/Isar/method.ML	Tue Nov 17 14:26:32 1998 +0100
+++ b/src/Pure/Isar/method.ML	Wed Nov 18 10:56:38 1998 +0100
@@ -218,11 +218,8 @@
 
 
 fun sectioned_args args ss f src ctxt =
-  let val (ctxt', (x, thss)) = syntax (sectioned args ss) ctxt src
-  in
-    warning "TRACE thms:"; seq Attribute.print_tthm (flat thss);             (* FIXME *)
-    f x ctxt'
-  end;
+  let val (ctxt', (x, _)) = syntax (sectioned args ss) ctxt src
+  in f x ctxt' end;
 
 fun default_sectioned_args att ss f src ctxt =
   sectioned_args thmss ss (fn ths => fn ctxt' => f (#1 (apply att (ctxt', ths)))) src ctxt;