# HG changeset patch
# User wenzelm
# Date 781956551 -3600
# Node ID f9a3f77f71e84aebb4d78260c00896e1785df25e
# Parent  8bc44f7bbab825c6d165306aa86f54f98d929017
fixed infix names in print_translations;

diff -r 8bc44f7bbab8 -r f9a3f77f71e8 src/ZF/ZF.thy
--- a/src/ZF/ZF.thy	Wed Oct 12 09:48:32 1994 +0100
+++ b/src/ZF/ZF.thy	Wed Oct 12 11:09:11 1994 +0100
@@ -220,5 +220,5 @@
 (* 'Dependent' type operators *)
 
 val print_translation =
-  [("Pi", dependent_tr' ("@PROD", "->")),
-   ("Sigma", dependent_tr' ("@SUM", "*"))];
+  [("Pi", dependent_tr' ("@PROD", "op ->")),
+   ("Sigma", dependent_tr' ("@SUM", "op *"))];