src/HOL/List.thy

--- a/src/HOL/List.thy	Tue Jan 09 15:18:07 2001 +0100
+++ b/src/HOL/List.thy	Tue Jan 09 15:22:13 2001 +0100
@@ -177,7 +177,7 @@
  lexn :: "('a * 'a)set => nat => ('a list * 'a list)set"
 primrec
 "lexn r 0       = {}"
-"lexn r (Suc n) = (prod_fun (%(x,xs). x#xs) (%(x,xs). x#xs) `` (r <*lex*> lexn r n)) Int
+"lexn r (Suc n) = (prod_fun (%(x,xs). x#xs) (%(x,xs). x#xs) ` (r <*lex*> lexn r n)) Int
                   {(xs,ys). length xs = Suc n & length ys = Suc n}"
 
 constdefs