# HG changeset patch
# User wenzelm
# Date 969892310 -7200
# Node ID ff08faf26d58a033e9c53892b1b1196d0273a02a
# Parent  fefb958b52aae18b21696ae486782f95cf24e4b9
tuned replacements;

diff -r fefb958b52aa -r ff08faf26d58 lib/scripts/unsymbolize.pl
--- 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 = $_;