# HG changeset patch
# User wenzelm
# Date 1727123617 -7200
# Node ID b5bdcdbf5ec1cebc8a034d3396a4837b7291f6ec
# Parent  8e72f55295fd9caf41b0b698dc35ddf77e5e8419
proper 'no_syntax' (amending 8e72f55295fd);

diff -r 8e72f55295fd -r b5bdcdbf5ec1 src/HOL/Nominal/Examples/Fsub.thy
--- a/src/HOL/Nominal/Examples/Fsub.thy	Mon Sep 23 21:09:23 2024 +0200
+++ b/src/HOL/Nominal/Examples/Fsub.thy	Mon Sep 23 22:33:37 2024 +0200
@@ -17,7 +17,7 @@
 section \<open>Types for Names, Nominal Datatype Declaration for Types and Terms\<close>
 
 no_syntax
-  "_Map" :: "maplets => 'a \<rightharpoonup> 'b"  (\<open>(1[_])\<close>)
+  "_Map" :: "maplets => 'a \<rightharpoonup> 'b"  (\<open>(\<open>indent=1 notation=\<open>mixfix maplets\<close>\<close>[_])\<close>)
 
 text \<open>The main point of this solution is to use names everywhere (be they bound, 
   binding or free). In System \FSUB{} there are two kinds of names corresponding to 
diff -r 8e72f55295fd -r b5bdcdbf5ec1 src/HOL/Nominal/Examples/Pattern.thy
--- a/src/HOL/Nominal/Examples/Pattern.thy	Mon Sep 23 21:09:23 2024 +0200
+++ b/src/HOL/Nominal/Examples/Pattern.thy	Mon Sep 23 22:33:37 2024 +0200
@@ -5,7 +5,7 @@
 begin
 
 no_syntax
-  "_Map" :: "maplets => 'a \<rightharpoonup> 'b"  (\<open>(1[_])\<close>)
+  "_Map" :: "maplets => 'a \<rightharpoonup> 'b"  (\<open>(\<open>indent=1 notation=\<open>mixfix maplets\<close>\<close>[_])\<close>)
 
 atom_decl name