# HG changeset patch
# User haftmann
# Date 1179596131 -7200
# Node ID 761f37e0ccc5095723e18625623006cd8deab039
# Parent  6ea1dc78807ac34aa02b4fb93c321142ad81d9ba
improved aliassing

diff -r 6ea1dc78807a -r 761f37e0ccc5 src/Pure/Tools/codegen_names.ML
--- a/src/Pure/Tools/codegen_names.ML	Sat May 19 19:35:17 2007 +0200
+++ b/src/Pure/Tools/codegen_names.ML	Sat May 19 19:35:31 2007 +0200
@@ -49,18 +49,19 @@
       -- Scan.repeat ((Scan.many1 is_valid >> implode) --| junk) >> op ::);
   in explode #> scan_valids #> space_implode "_" 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;
+fun purify_op "op -->" = "implies"
+  | purify_op "{}" = "empty"
+  | 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 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