diff -r 8428d4699d58 -r 02b7c759159b src/ZF/ind_syntax.ML
--- a/src/ZF/ind_syntax.ML	Thu Apr 09 12:31:35 1998 +0200
+++ b/src/ZF/ind_syntax.ML	Fri Apr 10 13:15:28 1998 +0200
@@ -12,6 +12,9 @@
 structure Ind_Syntax =
 struct
 
+(*Print tracing messages during processing of "inductive" theory sections*)
+val trace = ref false;
+
 (** Abstract syntax definitions for ZF **)
 
 val iT = Type("i",[]);
@@ -124,3 +127,5 @@
 
 end;
 
+
+val trace_induct = Ind_Syntax.trace;