diff -r 71c8847b10db -r 6870ee668115 test/Tools/isac/ProgLang/listC.sml
--- a/test/Tools/isac/ProgLang/listC.sml	Sun Aug 28 12:32:57 2016 +0200
+++ b/test/Tools/isac/ProgLang/listC.sml	Thu Sep 08 13:28:36 2016 +0200
@@ -7,34 +7,34 @@
 "-----------------------------------------------------------------------------";
 "table of contents -----------------------------------------------------------";
 "-----------------------------------------------------------------------------";
-"----------- check 'type xlist' [||1, 2, 3||] --------------------------------";
+"----------- check 'type xlist' {||1, 2, 3||} --------------------------------";
 "--------------------- NTH ---------------------------------------------------";
 "--------------------- LENGTH ------------------------------------------------";
 "--------------------- tl ----------------------------------------------------";
 "-----------------------------------------------------------------------------";
 "-----------------------------------------------------------------------------";
 
-"----------- check 'type xlist' [||1, 2, 3||] --------------------------------";
-"----------- check 'type xlist' [||1, 2, 3||] --------------------------------";
-"----------- check 'type xlist' [||1, 2, 3||] --------------------------------";
+"----------- check 'type xlist' {||1, 2, 3||} --------------------------------";
+"----------- check 'type xlist' {||1, 2, 3||} --------------------------------";
+"----------- check 'type xlist' {||1, 2, 3||} --------------------------------";
 (* ML representation *)
-val t1 = @{term "[|| ||]"};
-val t2 = @{term "[||1,2,3||]"};
+val t1 = @{term "{|| ||}"};
+val t2 = @{term "{||1,2,3||}"};
 
 (* pretty printing *)
 if Print_Mode.setmp [] 
   (Syntax.string_of_term (Config.put show_markup false (Proof_Context.init_global @{theory}))) t1
-  = "[|| ||]"
-then () else error "CHANGED pretty printing of '[|| ||]'";
+  = "{|| ||}"
+then () else error "CHANGED pretty printing of '{|| ||}'";
 
 if Print_Mode.setmp [] 
   (Syntax.string_of_term (Config.put show_markup false (Proof_Context.init_global @{theory}))) t2
-  = "[||1::'a, 2::'a, 3::'a||]"
-then () else error "CHANGED pretty printing of '[||1,2,3||]'"
+  = "{|| 1::'a, 2::'a, 3::'a ||}"
+then () else error "CHANGED pretty printing of '{||1,2,3||}'"
 
 (* parsing *)
-Syntax.read_term_global @{theory} "[|| ||]";
-Syntax.read_term_global @{theory} "[||1,2,3||]";
+Syntax.read_term_global @{theory} "{|| ||}";
+Syntax.read_term_global @{theory} "{||1,2,3||}";
 
 "--------------------- NTH ---------------------------------------------------";
 "--------------------- NTH ---------------------------------------------------";