# 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