# HG changeset patch
# User wenzelm
# Date 979846712 -3600
# Node ID 0b3997a180dd9466cb1b2334d12a1c419794bf6b
# Parent  ad13abb0a2643f1a35bc57a5d5897f072aa5e493
infix \\\\;

diff -r ad13abb0a264 -r 0b3997a180dd src/Pure/Interface/proof_general.ML
--- a/src/Pure/Interface/proof_general.ML	Thu Jan 18 20:37:38 2001 +0100
+++ b/src/Pure/Interface/proof_general.ML	Thu Jan 18 20:38:32 2001 +0100
@@ -317,3 +317,7 @@
 
 
 end;
+
+(*this hack avoids problems with escapes in ML commands; required for
+  Proof General 3.2*)
+infix \\\\ val op \\\\ = op \\;