diff -r 890e983cb07b -r 8b165615ffe3 src/Pure/simplifier.ML
--- a/src/Pure/simplifier.ML	Mon Nov 11 20:00:53 2013 +0100
+++ b/src/Pure/simplifier.ML	Mon Nov 11 20:50:12 2013 +0100
@@ -8,8 +8,6 @@
 signature BASIC_SIMPLIFIER =
 sig
   include BASIC_RAW_SIMPLIFIER
-  val Addsimprocs: simproc list -> unit
-  val Delsimprocs: simproc list -> unit
   val simp_tac: Proof.context -> int -> tactic
   val asm_simp_tac: Proof.context -> int -> tactic
   val full_simp_tac: Proof.context -> int -> tactic
@@ -126,16 +124,6 @@
 val cong_del = attrib del_cong;
 
 
-(* global simprocs *)
-
-fun Addsimprocs args =
-  Theory.setup (map_theory_simpset (fn ctxt => ctxt addsimprocs args));
-
-fun Delsimprocs args =
-  Theory.setup (map_theory_simpset (fn ctxt => ctxt delsimprocs args));
-
-
-
 (** named simprocs **)
 
 structure Simprocs = Generic_Data