src/HOL/Library/Nested_Environment.thy

         [] => Some (Env b es)
       | y # ys => lookup_option (es y) ys)"
   | "lookup_option None xs = None"
   | "lookup_option (Some e) xs = lookup e xs"
 
-hide const lookup_option
+hide_const lookup_option
 
 text {*
   \medskip The characteristic cases of @{term lookup} are expressed by
   the following equalities.
 *}

   | "update_option xs opt None =
       (if xs = [] then opt else None)"
   | "update_option xs opt (Some e) =
       (if xs = [] then opt else Some (update xs opt e))"
 
-hide const update_option
+hide_const update_option
 
 text {*
   \medskip The characteristic cases of @{term update} are expressed by
   the following equalities.
 *}