update_thy_only: setmp Thm.trace_simp false;
authorwenzelm
Wed, 07 Jun 2000 14:19:10 +0200
changeset 9050 578730810638
parent 9049 8a3101b62c4f
child 9051 887a15590f0e
update_thy_only: setmp Thm.trace_simp false;
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