src/HOL/Library/FuncSet.thy

--- a/src/HOL/Library/FuncSet.thy	Tue May 16 21:32:56 2006 +0200
+++ b/src/HOL/Library/FuncSet.thy	Tue May 16 21:33:01 2006 +0200
@@ -23,9 +23,8 @@
   funcset :: "['a set, 'b set] => ('a => 'b) set"      (infixr "->" 60)
   "A -> B == Pi A (%_. B)"
 
-abbreviation (xsymbols)
-  funcset1  (infixr "\<rightarrow>" 60)
-  "funcset1 == funcset"
+const_syntax (xsymbols)
+  funcset  (infixr "\<rightarrow>" 60)
 
 syntax
   "@Pi"  :: "[pttrn, 'a set, 'b set] => ('a => 'b) set"  ("(3PI _:_./ _)" 10)