diff -r 19b47bfac6ef -r 9e7d1c139569 src/Pure/Isar/isar_cmd.ML
--- a/src/Pure/Isar/isar_cmd.ML	Tue Apr 16 17:54:14 2013 +0200
+++ b/src/Pure/Isar/isar_cmd.ML	Thu Apr 18 17:07:01 2013 +0200
@@ -193,7 +193,7 @@
 fun simproc_setup name lhss (txt, pos) identifier =
   ML_Lex.read pos txt
   |> ML_Context.expression pos
-    "val proc: Morphism.morphism -> Simplifier.simpset -> cterm -> thm option"
+    "val proc: Morphism.morphism -> Proof.context -> cterm -> thm option"
     ("Context.map_proof (Simplifier.def_simproc_cmd {name = " ^ ML_Syntax.make_binding name ^ ", \
       \lhss = " ^ ML_Syntax.print_strings lhss ^ ", proc = proc, \
       \identifier = Library.maps ML_Context.thms " ^ ML_Syntax.print_strings identifier ^ "})")