changeset 10417 | 42e6b8502d52 |
parent 10246 | d8c968e6329a |
child 10933 | 0b3997a180dd |
--- a/src/Pure/Interface/proof_general.ML Tue Nov 07 17:52:12 2000 +0100 +++ b/src/Pure/Interface/proof_general.ML Tue Nov 07 17:53:12 2000 +0100 @@ -145,7 +145,7 @@ (* prepare theory context *) val thy_name = Path.pack o Path.drop_ext o Path.base o Path.unpack; -val update_thy_only = setmp Thm.trace_simp false ThyInfo.update_thy_only; +val update_thy_only = setmp MetaSimplifier.trace_simp false ThyInfo.update_thy_only; fun which_context () = (case Context.get_context () of