# HG changeset patch
# User wenzelm
# Date 1755354881 -7200
# Node ID fa6c4ad21a240aa7dab2bf588f254e492b2b5cdb
# Parent  8a97dc81c5380c4660bd760f54f93c2afcaeef71
tuned comments;

diff -r 8a97dc81c538 -r fa6c4ad21a24 src/Pure/context.ML
--- a/src/Pure/context.ML	Sat Aug 16 16:29:20 2025 +0200
+++ b/src/Pure/context.ML	Sat Aug 16 16:34:41 2025 +0200
@@ -1,14 +1,19 @@
 (*  Title:      Pure/context.ML
-    Author:     Markus Wenzel, TU Muenchen
+    Author:     Makarius
 
-Generic theory contexts with unique identity, arbitrarily typed data,
-monotonic development graph and history support.  Generic proof
-contexts with arbitrarily typed data.
+Generic theory contexts with unique identity, arbitrarily typed data, and
+monotonic updates.
 
-Firm naming conventions:
+Generic proof contexts with arbitrarily typed data.
+
+Good names:
    thy, thy', thy1, thy2: theory
    ctxt, ctxt', ctxt1, ctxt2: Proof.context
    context: Context.generic
+
+Bad names:
+  ctx: Proof.context
+  context: Proof.context
 *)
 
 signature BASIC_CONTEXT =