proper pattern (amending 40a365360680);
authorwenzelm
Thu, 03 Nov 2022 16:08:28 +0100
changeset 76414 cda63f26d0cb
parent 76413 e4f164d864dc
child 76415 f362975e8ba1
proper pattern (amending 40a365360680);
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