traceIt: plain term;

--- a/src/ZF/ind_syntax.ML	Tue Oct 25 18:18:58 2005 +0200
+++ b/src/ZF/ind_syntax.ML	Tue Oct 25 18:18:59 2005 +0200
@@ -15,9 +15,10 @@
 (*Print tracing messages during processing of "inductive" theory sections*)
 val trace = ref false;
 
-fun traceIt msg ct = 
-    if !trace then (writeln (msg ^ string_of_cterm ct); ct)
-    else ct;
+fun traceIt msg thy t = 
+  if !trace then (tracing (msg ^ Sign.string_of_term thy t); t)
+  else t;
+
 
 (** Abstract syntax definitions for ZF **)