dropped legacy
authorhaftmann
Sun, 13 May 2007 18:15:30 +0200
changeset 22953 cf78004a86f6
parent 22952 5b7259f3654e
child 22954 372e3471fca2
dropped legacy
src/Pure/Tools/codegen_names.ML
--- 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;