# HG changeset patch
# User haftmann
# Date 1179072930 -7200
# Node ID cf78004a86f6e4b977baa4293a2d483db6f144b3
# Parent  5b7259f3654e9dae7ce158e82d15b23e57322318
dropped legacy

diff -r 5b7259f3654e -r cf78004a86f6 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;