# HG changeset patch
# User wenzelm
# Date 1171660396 -3600
# Node ID 3ddd31fa45fdb40e910f2d7a11e20bc6f4472d76
# Parent  7df6bc8cf0b027fa4a35ad5c6789aed8e140d8fd
ML text: informative Output.debug only;

diff -r 7df6bc8cf0b0 -r 3ddd31fa45fd src/Pure/Thy/ml_context.ML
--- a/src/Pure/Thy/ml_context.ML	Fri Feb 16 22:13:15 2007 +0100
+++ b/src/Pure/Thy/ml_context.ML	Fri Feb 16 22:13:16 2007 +0100
@@ -160,7 +160,9 @@
 fun eval_wrapper name verbose txt =
   let
     val (txt1, txt2) = eval_antiquotes txt;
-    val _ = Output.debug (fn () => cat_lines [txt1, txt2]);
+    val _ =
+      if txt1 = isabelle_struct0 andalso txt2 = txt then ()
+      else Output.debug (fn () => cat_lines [txt1, txt2]);
   in eval "" false txt1; eval name verbose txt2; eval "" false isabelle_struct0 end;
 
 end;