added parse rules for -> and *;
removed ndependent_tr;

--- a/src/CCL/Type.thy	Mon Oct 04 15:44:29 1993 +0100
+++ b/src/CCL/Type.thy	Mon Oct 04 15:44:54 1993 +0100
@@ -35,7 +35,9 @@
 
 translations
   "PROD x:A. B" => "Pi(A, %x. B)"
+  "A -> B"      => "Pi(A, _K(B))"
   "SUM x:A. B"  => "Sigma(A, %x. B)"
+  "A * B"       => "Sigma(A, _K(B))"
   "{x: A. B}"   == "Subtype(A, %x. B)"
 
 rules
@@ -63,10 +65,6 @@
 
 ML
 
-val parse_translation =
-  [("@->", ndependent_tr "Pi"),
-   ("@*", ndependent_tr "Sigma")];
-
 val print_translation =
   [("Pi", dependent_tr' ("@Pi", "@->")),
    ("Sigma", dependent_tr' ("@Sigma", "@*"))];

--- a/src/CCL/type.thy	Mon Oct 04 15:44:29 1993 +0100
+++ b/src/CCL/type.thy	Mon Oct 04 15:44:54 1993 +0100
@@ -35,7 +35,9 @@
 
 translations
   "PROD x:A. B" => "Pi(A, %x. B)"
+  "A -> B"      => "Pi(A, _K(B))"
   "SUM x:A. B"  => "Sigma(A, %x. B)"
+  "A * B"       => "Sigma(A, _K(B))"
   "{x: A. B}"   == "Subtype(A, %x. B)"
 
 rules
@@ -63,10 +65,6 @@
 
 ML
 
-val parse_translation =
-  [("@->", ndependent_tr "Pi"),
-   ("@*", ndependent_tr "Sigma")];
-
 val print_translation =
   [("Pi", dependent_tr' ("@Pi", "@->")),
    ("Sigma", dependent_tr' ("@Sigma", "@*"))];