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 *"))];