# HG changeset patch
# User haftmann
# Date 1179567213 -7200
# Node ID 2ca26515625629e60dfbdab32baceae0f191ed7a
# Parent  db38b8046294b871fe6fcfdc6bda757716772054
dropped legacy

diff -r db38b8046294 -r 2ca265156256 src/Pure/Tools/codegen_names.ML
--- a/src/Pure/Tools/codegen_names.ML	Sat May 19 11:33:32 2007 +0200
+++ b/src/Pure/Tools/codegen_names.ML	Sat May 19 11:33:33 2007 +0200
@@ -49,21 +49,18 @@
       -- Scan.repeat ((Scan.many1 is_valid >> implode) --| junk) >> op ::);
   in explode #> scan_valids #> space_implode "_" end;
 
-fun purify_op "0" = "zero"
-  | purify_op "1" = "one"
-  | purify_op s =
-      let
-        fun rep_op "+" = SOME "plus"
-          | rep_op "*" = SOME "times"
-          | rep_op "&" = SOME "and"
-          | rep_op "|" = SOME "or"
-          | rep_op "=" = SOME "eq"
-          | rep_op "@" = SOME "append"
-          | rep_op "{" = SOME "empty"
-          | rep_op s = NONE;
-        val scan_valids = Symbol.scanner "Malformed input"
-           (Scan.repeat (Scan.some rep_op || Scan.one Symbol.not_eof));
-      in (explode #> scan_valids #> implode) s end;
+fun purify_op s =
+  let
+    fun rep_op "+" = SOME "plus"
+      | rep_op "*" = SOME "times"
+      | rep_op "&" = SOME "and"
+      | rep_op "|" = SOME "or"
+      | rep_op "=" = SOME "eq"
+      | rep_op "{" = SOME "empty"
+      | rep_op s = NONE;
+    val scan_valids = Symbol.scanner "Malformed input"
+       (Scan.repeat (Scan.some rep_op || Scan.one Symbol.not_eof));
+  in (explode #> scan_valids #> implode) s end;
 
 val purify_lower =
   explode