src/HOL/ex/Tarski.thy

--- a/src/HOL/ex/Tarski.thy	Mon Dec 10 20:58:15 2001 +0100
+++ b/src/HOL/ex/Tarski.thy	Mon Dec 10 20:59:43 2001 +0100
@@ -135,7 +135,7 @@
   Y_ss "Y <= P"
 defines
   intY1_def "intY1 == interval r (lub Y cl) (Top cl)"
-  v_def "v == glb {x. ((lam x: intY1. f x) x, x): induced intY1 r & x: intY1}
+  v_def "v == glb {x. ((%x: intY1. f x) x, x): induced intY1 r & x: intY1}
 	          (| pset=intY1, order=induced intY1 r|)"
 
 end