diff -r 718f10c8bbfc -r ecf1d5d87e5e src/HOL/HOLCF/Sfun.thy --- a/src/HOL/HOLCF/Sfun.thy Tue Oct 09 16:58:36 2012 +0200 +++ b/src/HOL/HOLCF/Sfun.thy Tue Oct 09 17:33:46 2012 +0200 @@ -8,7 +8,7 @@ imports Cfun begin -pcpodef (open) ('a, 'b) sfun (infixr "->!" 0) +pcpodef ('a, 'b) sfun (infixr "->!" 0) = "{f :: 'a \ 'b. f\\ = \}" by simp_all