src/HOL/Tools/record.ML
changeset 32091 30e2ffbba718
parent 31902 862ae16a799d
child 32212 21d7b4524395
     1.1 --- a/src/HOL/Tools/record.ML	Tue Jul 21 00:56:19 2009 +0200
     1.2 +++ b/src/HOL/Tools/record.ML	Tue Jul 21 01:03:18 2009 +0200
     1.3 @@ -105,7 +105,7 @@
     1.4  (* messages *)
     1.5  
     1.6  fun trace_thm str thm =
     1.7 -    tracing (str ^ (Pretty.string_of (Display.pretty_thm thm)));
     1.8 +    tracing (str ^ (Pretty.string_of (Display.pretty_thm_without_context thm)));
     1.9  
    1.10  fun trace_thms str thms =
    1.11      (tracing str; map (trace_thm "") thms);