# HG changeset patch
# User wenzelm
# Date 936212748 -7200
# Node ID fc8cad55af74384d41d07290f0d85fca5f454eca
# Parent  e94cbbe72c5d69f8b786ad735c856dabec62c3d5
isar: avoid verbose goal responses;

diff -r e94cbbe72c5d -r fc8cad55af74 src/Pure/Interface/proof_general.ML
--- a/src/Pure/Interface/proof_general.ML	Wed Sep 01 21:05:19 1999 +0200
+++ b/src/Pure/Interface/proof_general.ML	Wed Sep 01 21:05:48 1999 +0200
@@ -126,7 +126,8 @@
   if isar then
    (Toplevel.print_state_fn := plain_writeln Toplevel.print_state_default;
     Toplevel.prompt_state_fn := (suffix (oct_char "372") o Toplevel.prompt_state_default))
-  else Goals.print_current_goals_fn := print_current_goals);
+  else ();
+  Goals.print_current_goals_fn := print_current_goals);  (*isar: avoids verbose responses*)
 
 
 (* theory loader actions *)