diff -r de2d99b459b3 -r 384ac33802b0 src/Pure/simplifier.ML
--- a/src/Pure/simplifier.ML	Thu Dec 12 21:28:13 2013 +0100
+++ b/src/Pure/simplifier.ML	Thu Dec 12 22:38:25 2013 +0100
@@ -48,7 +48,7 @@
   val set_termless: (term * term -> bool) -> Proof.context -> Proof.context
   val set_subgoaler: (Proof.context -> int -> tactic) -> Proof.context -> Proof.context
   type trace_ops
-  val set_trace_ops: trace_ops -> Proof.context -> Proof.context
+  val set_trace_ops: trace_ops -> theory -> theory
   val simproc_global_i: theory -> string -> term list ->
     (Proof.context -> term -> thm option) -> simproc
   val simproc_global: theory -> string -> string list ->