# HG changeset patch
# User wenzelm
# Date 1191182118 -7200
# Node ID 102e0e732495a1594a737ea78bb6124c0af6a6a9
# Parent  5a3e336a2e371dd1ffe15202a899b61988749632
avoid unnamed infixes;

diff -r 5a3e336a2e37 -r 102e0e732495 src/HOL/ZF/HOLZF.thy
--- a/src/HOL/ZF/HOLZF.thy	Sun Sep 30 21:55:15 2007 +0200
+++ b/src/HOL/ZF/HOLZF.thy	Sun Sep 30 21:55:18 2007 +0200
@@ -194,8 +194,8 @@
   "Field A == union (Domain A) (Range A)"
 
 constdefs
-  "\<acute>"         :: "ZF \<Rightarrow> ZF => ZF"    (infixl 90) --{*function application*} 
-  app_def:  "f \<acute> x == (THE y. Elem (Opair x y) f)"
+  app :: "ZF \<Rightarrow> ZF => ZF"    (infixl "\<acute>" 90) --{*function application*} 
+  "f \<acute> x == (THE y. Elem (Opair x y) f)"
 
 constdefs
   isFun :: "ZF \<Rightarrow> bool"