# HG changeset patch
# User wenzelm
# Date 1458204081 -3600
# Node ID 1d1d7f5c0b277b48ae33f2ceafbc3223d9bd0929
# Parent  3cf0edded065b0ddb0e92136a5d52dc2e55dcd1f
proper ML type;

diff -r 3cf0edded065 -r 1d1d7f5c0b27 src/Doc/Isar_Ref/Generic.thy
--- a/src/Doc/Isar_Ref/Generic.thy	Thu Mar 17 08:56:45 2016 +0100
+++ b/src/Doc/Isar_Ref/Generic.thy	Thu Mar 17 09:41:21 2016 +0100
@@ -833,12 +833,12 @@
   procedure that is invoked by the Simplifier whenever any of the
   given term patterns match the current redex.  The implementation,
   which is provided as ML source text, needs to be of type @{ML_type
-  "morphism -> simpset -> cterm -> thm option"}, where the @{ML_type
+  "morphism -> Proof.context -> cterm -> thm option"}, where the @{ML_type
   cterm} represents the current redex \<open>r\<close> and the result is
   supposed to be some proven rewrite rule \<open>r \<equiv> r'\<close> (or a
   generalized version), or @{ML NONE} to indicate failure.  The
-  @{ML_type simpset} argument holds the full context of the current
-  Simplifier invocation, including the actual Isar proof context.  The
+  @{ML_type Proof.context} argument holds the full context of the current
+  Simplifier invocation.  The
   @{ML_type morphism} informs about the difference of the original
   compilation context wrt.\ the one of the actual application later
   on.  The optional @{keyword "identifier"} specifies theorems that