--- a/src/Pure/simplifier.ML Thu Dec 12 17:34:50 2013 +0100
+++ b/src/Pure/simplifier.ML Thu Dec 12 21:14:33 2013 +0100
@@ -47,6 +47,8 @@
val set_mkeqTrue: (Proof.context -> thm -> thm option) -> Proof.context -> Proof.context
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 simproc_global_i: theory -> string -> term list ->
(Proof.context -> term -> thm option) -> simproc
val simproc_global: theory -> string -> string list ->