# HG changeset patch
# User wenzelm
# Date 1008074580 -3600
# Node ID 624a8cd51b4ee8d411ddd3da95b325d7d6915d47
# Parent  6978ab7cac641235ff11767f25c6279c9e157e62
oops;

diff -r 6978ab7cac64 -r 624a8cd51b4e src/HOL/Fun.thy
--- a/src/HOL/Fun.thy	Mon Dec 10 20:59:43 2001 +0100
+++ b/src/HOL/Fun.thy	Tue Dec 11 13:43:00 2001 +0100
@@ -77,7 +77,7 @@
   funcset :: "['a set, 'b set] => ('a => 'b) set"      (infixr 60)
   "@lam" :: "[pttrn, 'a set, 'a => 'b] => ('a => 'b)"  ("(3%_:_./ _)" [0, 0, 3] 3)
 syntax (xsymbols)
-  "@lam" :: "[pttrn, 'a set, 'a => 'b] => ('a => 'b)"  ("(3\\<lambda>_\<in>_./ _)" [0, 0, 3] 3)
+  "@lam" :: "[pttrn, 'a set, 'a => 'b] => ('a => 'b)"  ("(3\\<lambda>_\\<in>_./ _)" [0, 0, 3] 3)
 
   (*Giving funcset an arrow syntax (-> or =>) clashes with many existing theories*)