# HG changeset patch
# User wenzelm
# Date 1667488108 -3600
# Node ID cda63f26d0cb77ce8da3b2c82f95dd3e69543611
# Parent  e4f164d864dc9fb5b87df1a9f8bc296409d83321
proper pattern (amending 40a365360680);

diff -r e4f164d864dc -r cda63f26d0cb src/Pure/PIDE/document.ML
--- a/src/Pure/PIDE/document.ML	Thu Nov 03 16:03:44 2022 +0100
+++ b/src/Pure/PIDE/document.ML	Thu Nov 03 16:08:28 2022 +0100
@@ -211,7 +211,7 @@
 fun theory_keywords name =
   (case Thy_Info.lookup_theory name of
     SOME thy => Thy_Header.get_keywords thy
-  | None => Keyword.empty_keywords);
+  | NONE => Keyword.empty_keywords);
 
 fun node_keywords name node =
   (case node of