src/HOL/Library/Type_Length.thy
changeset 69593 3dda49e08b9d
parent 64113 86efd3d4dc98
child 69597 ff784d5a5bfb
     1.1 --- a/src/HOL/Library/Type_Length.thy	Fri Jan 04 21:49:06 2019 +0100
     1.2 +++ b/src/HOL/Library/Type_Length.thy	Fri Jan 04 23:22:53 2019 +0100
     1.3 @@ -24,9 +24,9 @@
     1.4  
     1.5  print_translation \<open>
     1.6    let
     1.7 -    fun len_of_itself_tr' ctxt [Const (@{const_syntax Pure.type}, Type (_, [T]))] =
     1.8 -      Syntax.const @{syntax_const "_type_length"} $ Syntax_Phases.term_of_typ ctxt T
     1.9 -  in [(@{const_syntax len_of}, len_of_itself_tr')] end
    1.10 +    fun len_of_itself_tr' ctxt [Const (\<^const_syntax>\<open>Pure.type\<close>, Type (_, [T]))] =
    1.11 +      Syntax.const \<^syntax_const>\<open>_type_length\<close> $ Syntax_Phases.term_of_typ ctxt T
    1.12 +  in [(\<^const_syntax>\<open>len_of\<close>, len_of_itself_tr')] end
    1.13  \<close>
    1.14  
    1.15  text \<open>Some theorems are only true on words with length greater 0.\<close>