1.1 --- a/src/HOL/Lambda/ListOrder.thy	Fri Nov 17 02:19:55 2006 +0100
     1.2 +++ b/src/HOL/Lambda/ListOrder.thy	Fri Nov 17 02:20:03 2006 +0100
     1.3 @@ -14,7 +14,7 @@
     1.4  *}
     1.5  
     1.6  definition
     1.7 -  step1 :: "('a \<times> 'a) set => ('a list \<times> 'a list) set"
     1.8 +  step1 :: "('a \<times> 'a) set => ('a list \<times> 'a list) set" where
     1.9    "step1 r =
    1.10      {(ys, xs). \<exists>us z z' vs. xs = us @ z # vs \<and> (z', z) \<in> r \<and> ys =
    1.11        us @ z' # vs}"