author | haftmann |
Sun, 13 May 2007 18:15:30 +0200 | |
changeset 22953 | cf78004a86f6 |
parent 22952 | 5b7259f3654e |
child 22954 | 372e3471fca2 |
--- a/src/Pure/Tools/codegen_names.ML Sun May 13 18:15:28 2007 +0200 +++ b/src/Pure/Tools/codegen_names.ML Sun May 13 18:15:30 2007 +0200 @@ -54,13 +54,10 @@ | purify_op s = let fun rep_op "+" = SOME "plus" - | rep_op "-" = SOME "minus" | rep_op "*" = SOME "times" - | rep_op "/" = SOME "divide" | rep_op "&" = SOME "and" | rep_op "|" = SOME "or" | rep_op "=" = SOME "eq" - | rep_op "~" = SOME "inv" | rep_op "@" = SOME "append" | rep_op "{" = SOME "empty" | rep_op s = NONE;