src/Pure/Tools/nbe.ML
changeset 21991 04528ce9ded5
parent 21708 45e7491bea47
child 22033 8e19bad4125f
     1.1 --- a/src/Pure/Tools/nbe.ML	Thu Jan 04 14:01:40 2007 +0100
     1.2 +++ b/src/Pure/Tools/nbe.ML	Thu Jan 04 14:01:41 2007 +0100
     1.3 @@ -114,12 +114,12 @@
     1.4          with implicit side effect *)
     1.5      fun use_code NONE = ()
     1.6        | use_code (SOME s) =
     1.7 -          (tracing (fn () => "\n---generated code:\n" ^ s);
     1.8 +          (tracing (fn () => "\n---generated code:\n" ^ s) ();
     1.9             use_text (Output.tracing o enclose "\n---compiler echo:\n" "\n---\n",
    1.10                  Output.tracing o enclose "\n--- compiler echo (with error!):\n" "\n---\n")
    1.11              (!trace) s);
    1.12  
    1.13 -    val _ = tracing (fn () => "new definitions: " ^ (commas o maps (map fst)) funs);
    1.14 +    val _ = tracing (fn () => "new definitions: " ^ (commas o maps (map fst)) funs) ();
    1.15      val _ = tab := NBE_Data.get thy;;
    1.16      val _ = Library.seq (use_code o NBE_Codegen.generate thy
    1.17        (fn s => Symtab.defined (!tab) s)) funs;