src/Pure/simplifier.ML
changeset 38715 6513ea67d95d
parent 37441 69ba3f21c295
child 41226 adcb9a1198e7
--- 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