# 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}*) \