# HG changeset patch
# User wenzelm
# Date 968969796 -7200
# Node ID 5a96261189419e94285e0f81a4914ab29137124f
# Parent  07521b6eb888a4d0d8bfe615bda5f3ae8019d21f
updated;

diff -r 07521b6eb888 -r 5a9626118941 lib/scripts/feeder.pl
--- a/lib/scripts/feeder.pl	Fri Sep 15 00:16:08 2000 +0200
+++ b/lib/scripts/feeder.pl	Fri Sep 15 00:16:36 2000 +0200
@@ -91,7 +91,7 @@
   "\xe9", "\\<Leftarrow>",
   "\xea", "\\<Midarrow>",
   "\xeb", "\\<Rightarrow>",
-  "\xec", "\\<bow>",
+  "\xec", "\\<frown>",
   "\xed", "\\<mapsto>",
   "\xee", "\\<leadsto>",
   "\xef", "\\<up>",
diff -r 07521b6eb888 -r 5a9626118941 lib/scripts/symbolinput.pl
--- a/lib/scripts/symbolinput.pl	Fri Sep 15 00:16:08 2000 +0200
+++ b/lib/scripts/symbolinput.pl	Fri Sep 15 00:16:36 2000 +0200
@@ -84,7 +84,7 @@
   "\xe9", "\\<Leftarrow>",
   "\xea", "\\<Midarrow>",
   "\xeb", "\\<Rightarrow>",
-  "\xec", "\\<bow>",
+  "\xec", "\\<frown>",
   "\xed", "\\<mapsto>",
   "\xee", "\\<leadsto>",
   "\xef", "\\<up>",
diff -r 07521b6eb888 -r 5a9626118941 src/Pure/General/symbol.ML
--- a/src/Pure/General/symbol.ML	Fri Sep 15 00:16:08 2000 +0200
+++ b/src/Pure/General/symbol.ML	Fri Sep 15 00:16:36 2000 +0200
@@ -202,7 +202,7 @@
   "\\<Leftarrow>",
   "\\<Midarrow>",
   "\\<Rightarrow>",
-  "\\<bow>",
+  "\\<frown>",
   "\\<mapsto>",
   "\\<leadsto>",
   "\\<up>",