# HG changeset patch
# User wenzelm
# Date 1729254913 -7200
# Node ID 10e3a30b2512c4474167bc1bbae1eade8a95423d
# Parent  fc5066122e68f583a4d6b95792094e05b5598f1e
tuned;

diff -r fc5066122e68 -r 10e3a30b2512 src/HOL/Library/Type_Length.thy
--- a/src/HOL/Library/Type_Length.thy	Fri Oct 18 14:20:09 2024 +0200
+++ b/src/HOL/Library/Type_Length.thy	Fri Oct 18 14:35:13 2024 +0200
@@ -17,14 +17,9 @@
 class len0 =
   fixes len_of :: "'a itself \<Rightarrow> nat"
 
-syntax "_type_length" :: "type \<Rightarrow> nat" (\<open>(1LENGTH/(1'(_')))\<close>)
-
-syntax_consts
-  "_type_length" \<rightleftharpoons> len_of
-
-translations "LENGTH('a)" \<rightharpoonup>
-  "CONST len_of (CONST Pure.type :: 'a itself)"
-
+syntax "_type_length" :: "type \<Rightarrow> nat"  (\<open>(1LENGTH/(1'(_')))\<close>)
+syntax_consts "_type_length" \<rightleftharpoons> len_of
+translations "LENGTH('a)" \<rightharpoonup> "CONST len_of TYPE('a)"
 print_translation \<open>
   let
     fun len_of_itself_tr' ctxt [Const (\<^const_syntax>\<open>Pure.type\<close>, Type (_, [T]))] =