1.1 --- a/src/HOL/Tools/record_package.ML	Wed Feb 27 15:35:43 2008 +0100
     1.2 +++ b/src/HOL/Tools/record_package.ML	Wed Feb 27 16:07:55 2008 +0100
     1.3 @@ -994,9 +994,7 @@
     1.4    let
     1.5       val ss = HOL_basic_ss addsimps K_comp_convs; 
     1.6       val rhs = thm |> Thm.cprop_of |> Thm.dest_comb |> snd;
     1.7 -     val _ = tracing ("rhs:"^(Pretty.string_of (Display.pretty_cterm rhs)));
     1.8       val rhs' = (Simplifier.rewrite ss rhs);
     1.9 -     val _ = tracing ("rhs':"^(Pretty.string_of (Display.pretty_thm rhs')));
    1.10    in Thm.transitive thm rhs' end;
    1.11  in
    1.12  (* record_simproc *)