# HG changeset patch # User wenzelm # Date 963773396 -7200 # Node ID 1b2cd40579c615a78e3f12d7830dfdba1ab55a93 # Parent 4e7e0eb01a6c75a456287833e97267fbc414e765 avoid 'split'; diff -r 4e7e0eb01a6c -r 1b2cd40579c6 src/HOL/List.thy --- a/src/HOL/List.thy Sun Jul 16 20:49:33 2000 +0200 +++ b/src/HOL/List.thy Sun Jul 16 20:49:56 2000 +0200 @@ -177,7 +177,7 @@ lexn :: "('a * 'a)set => nat => ('a list * 'a list)set" primrec "lexn r 0 = {}" -"lexn r (Suc n) = (prod_fun (split op#) (split op#) `` (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