diff -r bd4ecd48c21f -r adcb9a1198e7 src/Pure/simplifier.ML
--- a/src/Pure/simplifier.ML	Fri Dec 17 13:45:43 2010 +0100
+++ b/src/Pure/simplifier.ML	Fri Dec 17 14:09:37 2010 +0100
@@ -33,6 +33,9 @@
   val pretty_ss: Proof.context -> simpset -> Pretty.T
   val clear_ss: simpset -> simpset
   val debug_bounds: bool Unsynchronized.ref
+  val add_simp: thm -> simpset -> simpset
+  val del_simp: thm -> simpset -> simpset
+  val add_prems: thm list -> simpset -> simpset
   val inherit_context: simpset -> simpset -> simpset
   val the_context: simpset -> Proof.context
   val context: Proof.context -> simpset -> simpset