src/HOL/Tools/list_code.ML
changeset 38923 79d7f2b4cf71
parent 37881 096c8397c989
child 48072 ace701efe203
equal deleted inserted replaced
38922:ec2a8efd8990 38923:79d7f2b4cf71
    44       case Option.map (cons t1) (implode_list nil' cons' t2)
    44       case Option.map (cons t1) (implode_list nil' cons' t2)
    45        of SOME ts =>
    45        of SOME ts =>
    46             Code_Printer.literal_list literals (map (pr vars Code_Printer.NOBR) ts)
    46             Code_Printer.literal_list literals (map (pr vars Code_Printer.NOBR) ts)
    47         | NONE =>
    47         | NONE =>
    48             default_list (Code_Printer.infix_cons literals) (pr vars) fxy t1 t2;
    48             default_list (Code_Printer.infix_cons literals) (pr vars) fxy t1 t2;
    49   in Code_Target.add_syntax_const target @{const_name Cons}
    49   in Code_Target.add_const_syntax target @{const_name Cons}
    50     (SOME (Code_Printer.complex_const_syntax (2, ([@{const_name Nil}, @{const_name Cons}], pretty))))
    50     (SOME (Code_Printer.complex_const_syntax (2, ([@{const_name Nil}, @{const_name Cons}], pretty))))
    51   end
    51   end
    52 
    52 
    53 end;
    53 end;