src/ZF/add_ind_def.ML
changeset 4804 02b7c759159b
parent 4352 7ac9f3e8a97d
child 4860 3692eb8a6cdb
     1.1 --- a/src/ZF/add_ind_def.ML	Thu Apr 09 12:31:35 1998 +0200
     1.2 +++ b/src/ZF/add_ind_def.ML	Fri Apr 10 13:15:28 1998 +0200
     1.3 @@ -165,8 +165,11 @@
     1.4               | _ => rec_tms ~~          (*define the sets as Parts*)
     1.5                      map (subst_atomic [(Free(X',iT),big_rec_tm)]) parts));
     1.6  
     1.7 -    val dummy = seq (writeln o Sign.string_of_term sign o #2) axpairs
     1.8 -  
     1.9 +    (*tracing: print the fixedpoint definition*)
    1.10 +    val _ = if !Ind_Syntax.trace then
    1.11 +		seq (writeln o Sign.string_of_term sign o #2) axpairs
    1.12 +            else ()
    1.13 +
    1.14    in  thy |> PureThy.add_store_defs_i axpairs  end
    1.15  
    1.16