# HG changeset patch
# User wenzelm
# Date 960380350 -7200
# Node ID 5787308106387f4fc531754e400bbdf8d998c131
# Parent  8a3101b62c4fbecd8327d080c5dafc1028f6fdea
update_thy_only: setmp Thm.trace_simp false;

diff -r 8a3101b62c4f -r 578730810638 src/Pure/Interface/proof_general.ML
--- a/src/Pure/Interface/proof_general.ML	Wed Jun 07 12:18:51 2000 +0200
+++ b/src/Pure/Interface/proof_general.ML	Wed Jun 07 14:19:10 2000 +0200
@@ -142,7 +142,7 @@
 (* prepare theory context *)
 
 val thy_name = Path.pack o Path.drop_ext o Path.base o Path.unpack;
-val update_thy_only = ThyInfo.update_thy_only;
+val update_thy_only = setmp Thm.trace_simp false ThyInfo.update_thy_only;
 
 fun which_context () =
   (case Context.get_context () of