--- a/src/Pure/simplifier.ML Wed Aug 25 18:19:04 2010 +0200
+++ b/src/Pure/simplifier.ML Wed Aug 25 18:36:22 2010 +0200
@@ -38,9 +38,9 @@
val context: Proof.context -> simpset -> simpset
val global_context: theory -> simpset -> simpset
val with_context: Proof.context -> (simpset -> simpset) -> simpset -> simpset
- val simproc_i: theory -> string -> term list
+ val simproc_global_i: theory -> string -> term list
-> (theory -> simpset -> term -> thm option) -> simproc
- val simproc: theory -> string -> string list
+ val simproc_global: theory -> string -> string list
-> (theory -> simpset -> term -> thm option) -> simproc
val rewrite: simpset -> conv
val asm_rewrite: simpset -> conv