isar: avoid verbose goal responses;
authorwenzelm
Wed, 01 Sep 1999 21:05:48 +0200
changeset 7407 fc8cad55af74
parent 7406 e94cbbe72c5d
child 7408 1ec1567c1307
isar: avoid verbose goal responses;
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 *)