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