1structure Symreltab = Table( 2 type key = string * string 3 val ord = Portable.pair_compare (String.compare, String.compare) 4 fun pp (s1,s2) = 5 let 6 open HOLPP Portable 7 in 8 block CONSISTENT 0 [ 9 add_string "(", 10 block CONSISTENT 1 [add_string (mlquote s1), add_string ",", 11 add_break (1,0), add_string (mlquote s2)], 12 add_string ")" 13 ] 14 end 15); 16