diff -r a033b5b6f544 -r 3a196e63a80d src/Pure/Pure.thy --- a/src/Pure/Pure.thy Sat Aug 03 13:12:58 2024 +0200 +++ b/src/Pure/Pure.thy Sun Aug 04 12:21:13 2024 +0200 @@ -605,7 +605,7 @@ val _ = hide_names \<^command_keyword>\hide_type\ "types" Sign.hide_type Parse.type_const - ((#1 o dest_Type) oo Proof_Context.read_type_name {proper = true, strict = false}); + (dest_Type_name oo Proof_Context.read_type_name {proper = true, strict = false}); val _ = hide_names \<^command_keyword>\hide_const\ "consts" Sign.hide_const Parse.const