src/Pure/Interface/proof_general.ML
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