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