equal
deleted
inserted
replaced
752 end |
752 end |
753 in add 0 |> apsnd SOME end |
753 in add 0 |> apsnd SOME end |
754 |
754 |
755 fun avoid_clash_with_dfg_keywords s = |
755 fun avoid_clash_with_dfg_keywords s = |
756 let val n = String.size s in |
756 let val n = String.size s in |
757 if n < 2 orelse String.isSubstring "_" s then |
757 if n < 2 orelse (n = 2 andalso String.sub (s, 0) = String.sub (s, 1)) orelse |
|
758 String.isSubstring "_" s then |
758 s |
759 s |
759 else |
760 else |
760 String.substring (s, 0, n - 1) ^ |
761 String.substring (s, 0, n - 1) ^ |
761 String.str (Char.toUpper (String.sub (s, n - 1))) |
762 String.str (Char.toUpper (String.sub (s, n - 1))) |
762 end |
763 end |