# HG changeset patch
# User schirmer
# Date 1204124875 -3600
# Node ID 429c1917f07b12af669582900421a582f9d8d9fd
# Parent  31e4ff2b9e5bb38712a8e67b017f25cdbc122d11
removed some debugging output from trace

diff -r 31e4ff2b9e5b -r 429c1917f07b src/HOL/Tools/record_package.ML
--- a/src/HOL/Tools/record_package.ML	Wed Feb 27 15:35:43 2008 +0100
+++ b/src/HOL/Tools/record_package.ML	Wed Feb 27 16:07:55 2008 +0100
@@ -994,9 +994,7 @@
   let
      val ss = HOL_basic_ss addsimps K_comp_convs; 
      val rhs = thm |> Thm.cprop_of |> Thm.dest_comb |> snd;
-     val _ = tracing ("rhs:"^(Pretty.string_of (Display.pretty_cterm rhs)));
      val rhs' = (Simplifier.rewrite ss rhs);
-     val _ = tracing ("rhs':"^(Pretty.string_of (Display.pretty_thm rhs')));
   in Thm.transitive thm rhs' end;
 in
 (* record_simproc *)