src/Pure/ML/ml_syntax.ML
changeset 41491 a2ad5b824051
parent 41415 23533273220a
child 42047 a7a4e04b5386
equal deleted inserted replaced
41490:0f1e411a1448 41491:a2ad5b824051
    47 
    47 
    48 (* literal output -- unformatted *)
    48 (* literal output -- unformatted *)
    49 
    49 
    50 val atomic = enclose "(" ")";
    50 val atomic = enclose "(" ")";
    51 
    51 
    52 val print_int = Int.toString;
    52 val print_int = string_of_int;
    53 
    53 
    54 fun print_pair f1 f2 (x, y) = "(" ^ f1 x ^ ", " ^ f2 y ^ ")";
    54 fun print_pair f1 f2 (x, y) = "(" ^ f1 x ^ ", " ^ f2 y ^ ")";
    55 
    55 
    56 fun print_list f = enclose "[" "]" o commas o map f;
    56 fun print_list f = enclose "[" "]" o commas o map f;
    57 
    57