diff -r 541f6367a431 -r b7870c2bd7df src/HOL/Import/Generate-HOL/GenHOL4Real.thy
--- a/src/HOL/Import/Generate-HOL/GenHOL4Real.thy	Wed Sep 28 11:50:15 2005 +0200
+++ b/src/HOL/Import/Generate-HOL/GenHOL4Real.thy	Wed Sep 28 13:17:23 2005 +0200
@@ -67,6 +67,9 @@
 end_import;
 
 import_theory seq;
+const_renames
+"-->" > "hol4-->";
+
 end_import;
 
 import_theory lim;