diff -r c2ee8f5a5652 -r 7e6cdcd113a2 src/HOL/Library/FuncSet.thy
--- a/src/HOL/Library/FuncSet.thy	Fri Sep 27 13:24:29 2002 +0200
+++ b/src/HOL/Library/FuncSet.thy	Fri Sep 27 16:44:50 2002 +0200
@@ -39,6 +39,7 @@
   compose :: "['a set, 'b => 'c, 'a => 'b] => ('a => 'c)"
   "compose A g f == \<lambda>x\<in>A. g (f x)"
 
+print_translation {* [("Pi", dependent_tr' ("@Pi", "funcset"))] *}
 
 
 subsection{*Basic Properties of @{term Pi}*}
@@ -105,7 +106,6 @@
 lemma restrict_in_funcset: "(!!x. x \<in> A ==> f x \<in> B) ==> (\<lambda>x\<in>A. f x) \<in> A -> B"
 by (simp add: Pi_def restrict_def)
 
-
 lemma restrictI: "(!!x. x \<in> A ==> f x \<in> B x) ==> (\<lambda>x\<in>A. f x) \<in> Pi A B"
 by (simp add: Pi_def restrict_def)