--- 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)]]);