update_thy_only: setmp Thm.trace_simp false;
authorwenzelm
Wed Jun 07 14:19:10 2000 +0200 (2000-06-07)
changeset 9050578730810638
parent 9049 8a3101b62c4f
child 9051 887a15590f0e
update_thy_only: setmp Thm.trace_simp false;
src/Pure/Interface/proof_general.ML
     1.1 --- a/src/Pure/Interface/proof_general.ML	Wed Jun 07 12:18:51 2000 +0200
     1.2 +++ b/src/Pure/Interface/proof_general.ML	Wed Jun 07 14:19:10 2000 +0200
     1.3 @@ -142,7 +142,7 @@
     1.4  (* prepare theory context *)
     1.5  
     1.6  val thy_name = Path.pack o Path.drop_ext o Path.base o Path.unpack;
     1.7 -val update_thy_only = ThyInfo.update_thy_only;
     1.8 +val update_thy_only = setmp Thm.trace_simp false ThyInfo.update_thy_only;
     1.9  
    1.10  fun which_context () =
    1.11    (case Context.get_context () of