--- a/lib/scripts/unsymbolize.pl Mon Sep 25 12:11:45 2000 +0200
+++ b/lib/scripts/unsymbolize.pl Mon Sep 25 16:31:50 2000 +0200
@@ -22,13 +22,15 @@
s/\\?\\<Midarrow>\\?\\<Rightarrow>/==>/g;
s/\\?\\<Rightarrow>/=>/g;
s/\\?\\<equiv>/==/g;
- s/\\?\\<lbrakk>/[|/g;
- s/\\?\\<rbrakk>/|]/g;
+ s/\\?\\<lbrakk> ?/[| /g;
+ s/\\?\\ ?<rbrakk>/ |]/g;
+ s/\\?\\<lparr> ?/(| /g;
+ s/\\?\\ ?<rparr>/ |)/g;
# HOL
s/\\?\\<longrightarrow>/-->/g;
s/\\?\\<midarrow>\\?\\<rightarrow>/-->/g;
s/\\?\\<rightarrow>/->/g;
- s/\\?\\<epsilon>\s*/SOME /g;
+ s/\\?\\<epsilon> ?/SOME /g;
$result = $_;