--- 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 \\;