src/Pure/Isar/locale.ML
changeset 18708 4b3dadb4fe33
parent 18698 a95c2adc8900
child 18728 6790126ab5f6
     1.1 --- a/src/Pure/Isar/locale.ML	Thu Jan 19 15:45:10 2006 +0100
     1.2 +++ b/src/Pure/Isar/locale.ML	Thu Jan 19 21:22:08 2006 +0100
     1.3 @@ -278,7 +278,7 @@
     1.4      |> Pretty.writeln;
     1.5  end);
     1.6  
     1.7 -val _ = Context.add_setup [GlobalLocalesData.init];
     1.8 +val _ = Context.add_setup GlobalLocalesData.init;
     1.9  
    1.10  
    1.11  
    1.12 @@ -293,7 +293,7 @@
    1.13    fun print _ _ = ();
    1.14  end);
    1.15  
    1.16 -val _ = Context.add_setup [LocalLocalesData.init];
    1.17 +val _ = Context.add_setup LocalLocalesData.init;
    1.18  
    1.19  
    1.20  (* access locales *)
    1.21 @@ -1718,8 +1718,8 @@
    1.22  end;
    1.23  
    1.24  val _ = Context.add_setup
    1.25 - [add_locale_i true "var" empty [Fixes [(Syntax.internal "x", NONE, NoSyn)]],
    1.26 -  add_locale_i true "struct" empty [Fixes [(Syntax.internal "S", NONE, Structure)]]];
    1.27 + (add_locale_i true "var" empty [Fixes [(Syntax.internal "x", NONE, NoSyn)]] #>
    1.28 +  add_locale_i true "struct" empty [Fixes [(Syntax.internal "S", NONE, Structure)]]);
    1.29  
    1.30  
    1.31