--- 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 ->