1.1 --- a/test/Tools/isac/ProgLang/listC.sml	Sun Aug 28 12:32:57 2016 +0200
     1.2 +++ b/test/Tools/isac/ProgLang/listC.sml	Thu Sep 08 13:28:36 2016 +0200
     1.3 @@ -7,34 +7,34 @@
     1.4  "-----------------------------------------------------------------------------";
     1.5  "table of contents -----------------------------------------------------------";
     1.6  "-----------------------------------------------------------------------------";
     1.7 -"----------- check 'type xlist' [||1, 2, 3||] --------------------------------";
     1.8 +"----------- check 'type xlist' {||1, 2, 3||} --------------------------------";
     1.9  "--------------------- NTH ---------------------------------------------------";
    1.10  "--------------------- LENGTH ------------------------------------------------";
    1.11  "--------------------- tl ----------------------------------------------------";
    1.12  "-----------------------------------------------------------------------------";
    1.13  "-----------------------------------------------------------------------------";
    1.14  
    1.15 -"----------- check 'type xlist' [||1, 2, 3||] --------------------------------";
    1.16 -"----------- check 'type xlist' [||1, 2, 3||] --------------------------------";
    1.17 -"----------- check 'type xlist' [||1, 2, 3||] --------------------------------";
    1.18 +"----------- check 'type xlist' {||1, 2, 3||} --------------------------------";
    1.19 +"----------- check 'type xlist' {||1, 2, 3||} --------------------------------";
    1.20 +"----------- check 'type xlist' {||1, 2, 3||} --------------------------------";
    1.21  (* ML representation *)
    1.22 -val t1 = @{term "[|| ||]"};
    1.23 -val t2 = @{term "[||1,2,3||]"};
    1.24 +val t1 = @{term "{|| ||}"};
    1.25 +val t2 = @{term "{||1,2,3||}"};
    1.26  
    1.27  (* pretty printing *)
    1.28  if Print_Mode.setmp [] 
    1.29    (Syntax.string_of_term (Config.put show_markup false (Proof_Context.init_global @{theory}))) t1
    1.30 -  = "[|| ||]"
    1.31 -then () else error "CHANGED pretty printing of '[|| ||]'";
    1.32 +  = "{|| ||}"
    1.33 +then () else error "CHANGED pretty printing of '{|| ||}'";
    1.34  
    1.35  if Print_Mode.setmp [] 
    1.36    (Syntax.string_of_term (Config.put show_markup false (Proof_Context.init_global @{theory}))) t2
    1.37 -  = "[||1::'a, 2::'a, 3::'a||]"
    1.38 -then () else error "CHANGED pretty printing of '[||1,2,3||]'"
    1.39 +  = "{|| 1::'a, 2::'a, 3::'a ||}"
    1.40 +then () else error "CHANGED pretty printing of '{||1,2,3||}'"
    1.41  
    1.42  (* parsing *)
    1.43 -Syntax.read_term_global @{theory} "[|| ||]";
    1.44 -Syntax.read_term_global @{theory} "[||1,2,3||]";
    1.45 +Syntax.read_term_global @{theory} "{|| ||}";
    1.46 +Syntax.read_term_global @{theory} "{||1,2,3||}";
    1.47  
    1.48  "--------------------- NTH ---------------------------------------------------";
    1.49  "--------------------- NTH ---------------------------------------------------";