# HG changeset patch
# User oheimb
# Date 878650671 -3600
# Node ID 390e10ddadf2fea3042e4c0256fd180fa5f106f0
# Parent  57c1e7d709601529285bf98f1d0f70f851185e17
simplified (and corrected) syntax definition of fapp

diff -r 57c1e7d70960 -r 390e10ddadf2 src/HOLCF/Cfun1.thy
--- a/src/HOLCF/Cfun1.thy	Tue Nov 04 14:09:37 1997 +0100
+++ b/src/HOLCF/Cfun1.thy	Tue Nov 04 14:37:51 1997 +0100
@@ -17,17 +17,14 @@
 instance "->"  :: (cpo,cpo)sq_ord
 
 consts  
-        fapp      :: "('a -> 'b)=>('a => 'b)"   (* usually Rep_Cfun *)
+        fapp      :: "('a -> 'b)=>('a => 'b)" ("_`_" [999,1000] 999)
+					        (* usually Rep_Cfun *)
                                                 (* application      *)
         fabs      :: "('a => 'b)=>('a -> 'b)"     (binder "LAM " 10)
                                                 (* usually Abs_Cfun *)
                                                 (* abstraction      *)
         less_cfun :: "[('a -> 'b),('a -> 'b)]=>bool"
 
-syntax  "@fapp"   :: "('a -> 'b)=>('a => 'b)" ("_`_" [999,1000] 999)
-
-translations "f`x" == "fapp f x"
-
 syntax (symbols)
   "->"		:: [type, type] => type	("(_ \\<rightarrow>/ _)" [1,0]0)
   "LAM "	:: "[idts, 'a => 'b] => ('a -> 'b)"