# HG changeset patch
# User haftmann
# Date 1167915701 -3600
# Node ID 04528ce9ded58959c9768dbf3cd48f142c0f09c5
# Parent  d382f901304c935b7d54007fbf4bc8ebb4681635
fixed output

diff -r d382f901304c -r 04528ce9ded5 src/Pure/Tools/nbe.ML
--- a/src/Pure/Tools/nbe.ML	Thu Jan 04 14:01:40 2007 +0100
+++ b/src/Pure/Tools/nbe.ML	Thu Jan 04 14:01:41 2007 +0100
@@ -114,12 +114,12 @@
         with implicit side effect *)
     fun use_code NONE = ()
       | use_code (SOME s) =
-          (tracing (fn () => "\n---generated code:\n" ^ s);
+          (tracing (fn () => "\n---generated code:\n" ^ s) ();
            use_text (Output.tracing o enclose "\n---compiler echo:\n" "\n---\n",
                 Output.tracing o enclose "\n--- compiler echo (with error!):\n" "\n---\n")
             (!trace) s);
 
-    val _ = tracing (fn () => "new definitions: " ^ (commas o maps (map fst)) funs);
+    val _ = tracing (fn () => "new definitions: " ^ (commas o maps (map fst)) funs) ();
     val _ = tab := NBE_Data.get thy;;
     val _ = Library.seq (use_code o NBE_Codegen.generate thy
       (fn s => Symtab.defined (!tab) s)) funs;