src/Pure/Isar/locale.ML
changeset 18708 4b3dadb4fe33
parent 18698 a95c2adc8900
child 18728 6790126ab5f6
--- a/src/Pure/Isar/locale.ML	Thu Jan 19 15:45:10 2006 +0100
+++ b/src/Pure/Isar/locale.ML	Thu Jan 19 21:22:08 2006 +0100
@@ -278,7 +278,7 @@
     |> Pretty.writeln;
 end);
 
-val _ = Context.add_setup [GlobalLocalesData.init];
+val _ = Context.add_setup GlobalLocalesData.init;
 
 
 
@@ -293,7 +293,7 @@
   fun print _ _ = ();
 end);
 
-val _ = Context.add_setup [LocalLocalesData.init];
+val _ = Context.add_setup LocalLocalesData.init;
 
 
 (* access locales *)
@@ -1718,8 +1718,8 @@
 end;
 
 val _ = Context.add_setup
- [add_locale_i true "var" empty [Fixes [(Syntax.internal "x", NONE, NoSyn)]],
-  add_locale_i true "struct" empty [Fixes [(Syntax.internal "S", NONE, Structure)]]];
+ (add_locale_i true "var" empty [Fixes [(Syntax.internal "x", NONE, NoSyn)]] #>
+  add_locale_i true "struct" empty [Fixes [(Syntax.internal "S", NONE, Structure)]]);