proper syntax category;
authorwenzelm
Tue, 07 Dec 2021 19:32:43 +0100
changeset 74910 bdaf29253394
parent 74875 98d2b3375258
child 74911 74a800810bde
proper syntax category;
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>