# HG changeset patch
# User wenzelm
# Date 1028625592 -7200
# Node ID ced7a699282b5f0d45acde19289917050e07a97a
# Parent  83f41b047a39327ec8567246938f3e6f6547299e
predefined locales "var" and "struct" (useful for sharing parameters);

diff -r 83f41b047a39 -r ced7a699282b src/Pure/Isar/locale.ML
--- a/src/Pure/Isar/locale.ML	Tue Aug 06 11:19:00 2002 +0200
+++ b/src/Pure/Isar/locale.ML	Tue Aug 06 11:19:52 2002 +0200
@@ -990,6 +990,8 @@
 (** locale theory setup **)
 
 val setup =
- [LocalesData.init];
+ [LocalesData.init,
+  add_locale_i true "var" empty [Elem (Fixes [(Syntax.internal "x", None, Some Syntax.NoSyn)])],
+  add_locale_i true "struct" empty [Elem (Fixes [(Syntax.internal "S", None, None)])]];
 
 end;