# HG changeset patch
# User wenzelm
# Date 1237399886 -3600
# Node ID c12484a273678a840bf5c09447c87a034cfa8dc2
# Parent  8fac7efcce0ad12502d6dd27dfcc452816e44626
reduced verbosity;

diff -r 8fac7efcce0a -r c12484a27367 src/Pure/Isar/toplevel.ML
--- a/src/Pure/Isar/toplevel.ML	Wed Mar 18 15:23:52 2009 +0100
+++ b/src/Pure/Isar/toplevel.ML	Wed Mar 18 19:11:26 2009 +0100
@@ -647,11 +647,9 @@
 
 local
 
-fun app int (tr as Transition {trans, pos, int_only, print, no_timing, ...}) =
+fun app int (tr as Transition {trans, pos, print, no_timing, ...}) =
   setmp_thread_position tr (fn state =>
     let
-      val _ = if not int andalso int_only then warning (command_msg "Interactive-only " tr) else ();
-
       fun do_timing f x = (warning (command_msg "" tr); timeap f x);
       fun do_profiling f x = profile (! profiling) f x;