# HG changeset patch
# User wenzelm
# Date 1638901963 -3600
# Node ID bdaf29253394ad7c774aae0ef7f03d86be9f8bf4
# Parent  98d2b3375258493c82f28d012a0d7b70b1022420
proper syntax category;

diff -r 98d2b3375258 -r bdaf29253394 src/Doc/Implementation/Logic.thy
--- a/src/Doc/Implementation/Logic.thy	Sat Dec 04 12:38:32 2021 +0100
+++ b/src/Doc/Implementation/Logic.thy	Tue Dec 07 19:32:43 2021 +0100
@@ -491,7 +491,7 @@
     @{syntax_def term_const}:
       @{syntax name} (@{syntax embedded_ml}*) (@{syntax for_args})?
     ;
-    @{syntax_def type_const_fn}: @{ syntax term_const} @'=>' @{syntax embedded}
+    @{syntax_def term_const_fn}: @{ syntax term_const} @'=>' @{syntax embedded}
     ;
     @{syntax_def for_args}: @'for' (@{syntax embedded_ml}*)
   \<close>