# HG changeset patch
# User ballarin
# Date 1154609637 -7200
# Node ID 6e070b33e72bbfcaa0c7d39cd59ead77699fd37f
# Parent  99b6e2900c0f354de76c57c4f0f999fc914e64fd
Updated comments.

diff -r 99b6e2900c0f -r 6e070b33e72b src/Pure/Isar/locale.ML
--- a/src/Pure/Isar/locale.ML	Thu Aug 03 14:53:35 2006 +0200
+++ b/src/Pure/Isar/locale.ML	Thu Aug 03 14:53:57 2006 +0200
@@ -32,8 +32,6 @@
 - beta-eta normalisation of interpretation parameters
 - dangling type frees in locales
 - test subsumption of interpretations when merging theories
-- var vs. fixes in locale to be interpreted (interpretation in locale)
-  (implicit locale expressions generated by multiple registrations)
 *)
 
 signature LOCALE =
@@ -160,7 +158,8 @@
 type locale =
  {axiom: Element.witness list,
     (* For locales that define predicates this is [A [A]], where A is the locale
-       specification.  Otherwise []. *)
+       specification.  Otherwise [].
+       Only required to generate the right witnesses for locales with predicates. *)
   import: expr,                                                     (*dynamic import*)
   elems: (Element.context_i * stamp) list,
     (* Static content, neither Fixes nor Constrains elements *)