src/Pure/Isar/locale.ML

   fun print _ (space, locs, _) =
     Pretty.strs ("locales:" :: map #1 (NameSpace.extern_table (space, locs)))
     |> Pretty.writeln;
 end);
 
-val _ = Context.add_setup [GlobalLocalesData.init];
+val _ = Context.add_setup GlobalLocalesData.init;
 
 
 
 (** context data **)
 

     (* registrations, indexed by locale name *)
   fun init _ = Symtab.empty;
   fun print _ _ = ();
 end);
 
-val _ = Context.add_setup [LocalLocalesData.init];
+val _ = Context.add_setup LocalLocalesData.init;
 
 
 (* access locales *)
 
 val print_locales = GlobalLocalesData.print;

 fun add_locale_i b = #2 oooo add_locale_context_i b;
 
 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)]]);
 
 
 
 (** locale goals **)