src/CCL/Term.thy

--- a/src/CCL/Term.thy	Thu Oct 10 12:19:50 2024 +0200
+++ b/src/CCL/Term.thy	Thu Oct 10 12:20:24 2024 +0200
@@ -131,7 +131,7 @@
 definition nrec :: "[i,i,[i,i]\<Rightarrow>i]\<Rightarrow>i"
   where "nrec(n,b,c) == letrec g x be ncase(x, b, \<lambda>y. c(y,g(y))) in g(n)"
 
-definition nil :: "i"  (\<open>([])\<close>)
+definition nil :: "i"  (\<open>[]\<close>)
   where "[] == inl(one)"
 
 definition cons :: "[i,i]\<Rightarrow>i"  (infixr \<open>$\<close> 80)