author | wenzelm |
Wed, 07 Jun 2000 14:19:10 +0200 | |
changeset 9050 | 578730810638 |
parent 9049 | 8a3101b62c4f |
child 9051 | 887a15590f0e |
--- 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