# HG changeset patch
# User blanchet
# Date 1411058998 -7200
# Node ID 0e8d82e95dd23e0e208e9e3020b9dcbac63ac2f9
# Parent  14404f6b760c85d38f10bf34addc5d876065f000
removed debugging junk

diff -r 14404f6b760c -r 0e8d82e95dd2 src/HOL/Tools/Old_Datatype/old_size.ML
--- a/src/HOL/Tools/Old_Datatype/old_size.ML	Thu Sep 18 17:54:56 2014 +0200
+++ b/src/HOL/Tools/Old_Datatype/old_size.ML	Thu Sep 18 18:49:58 2014 +0200
@@ -214,7 +214,6 @@
     val no_size = exists (fn (_, (_, _, constrs)) => exists (fn (_, cargs) => exists (fn dt =>
       Old_Datatype_Aux.is_rec_type dt andalso
         not (null (fst (Old_Datatype_Aux.strip_dtyp dt)))) cargs) constrs) descr
-val _ = tracing ("NAME: " ^ @{make_string} (name, no_size))(*###*)
   in
     if no_size then thy
     else