# HG changeset patch
# User wenzelm
# Date 869225763 -7200
# Node ID f4b28e25ba997198f606831b7cf4235417bc4b38
# Parent  b894f4c13df5a393f614a0eb3cee716759da7c01
renamed |-> <-| <-> to Parse/PrintRule;

diff -r b894f4c13df5 -r f4b28e25ba99 src/Pure/Thy/thy_parse.ML
--- a/src/Pure/Thy/thy_parse.ML	Fri Jul 18 13:35:36 1997 +0200
+++ b/src/Pure/Thy/thy_parse.ML	Fri Jul 18 13:36:03 1997 +0200
@@ -320,9 +320,9 @@
   optional ("(" $$-- !! (name --$$ ")")) "\"logic\"" -- string >> mk_pair;
 
 val trans_arrow =
-  $$ "=>" >> K "Syntax.|-> " ||
-  $$ "<=" >> K "Syntax.<-| " ||
-  $$ "==" >> K "Syntax.<-> ";
+  $$ "=>" >> K "Syntax.ParseRule " ||
+  $$ "<=" >> K "Syntax.PrintRule " ||
+  $$ "==" >> K "Syntax.ParsePrintRule ";
 
 val trans_line =
   trans_pat -- !! (trans_arrow -- trans_pat)