diff -r 5ddbdbadba06 -r 0848ab6fe5fc src/HOL/Induct/SList.thy
--- a/src/HOL/Induct/SList.thy	Thu Apr 22 11:02:22 2004 +0200
+++ b/src/HOL/Induct/SList.thy	Thu Apr 22 12:11:17 2004 +0200
@@ -79,16 +79,14 @@
   "Cons"       :: "['a, 'a list] => 'a list"           (infixr "#" 65)
    "x#xs == Abs_List(CONS (Leaf x)(Rep_List xs))"
 
-  list_case :: "['b, ['a, 'a list]=>'b, 'a list] => 'b"
-   "list_case a f xs == list_rec xs a (%x xs r. f x xs)"
-
   (* list Recursion -- the trancl is Essential; see list.ML *)
-
-
   list_rec  :: "['a list, 'b, ['a, 'a list, 'b]=>'b] => 'b"
    "list_rec l c d ==
       List_rec(Rep_List l) c (%x y r. d(inv Leaf x)(Abs_List y) r)"
 
+  list_case :: "['b, ['a, 'a list]=>'b, 'a list] => 'b"
+   "list_case a f xs == list_rec xs a (%x xs r. f x xs)"
+
 (* list Enumeration *)
 consts
   "[]"      :: "'a list"                            ("[]")
@@ -178,14 +176,14 @@
   "rev xs   == list_rec xs [] (%x xs xsa. xsa @ [x])"
 
 (* miscellaneous definitions *)
-  zip       :: "'a list * 'b list => ('a*'b) list"
-  "zip      == zipWith  (%s. s)"
-
   zipWith   :: "['a * 'b => 'c, 'a list * 'b list] => 'c list"
   "zipWith f S == (list_rec (fst S)  (%T.[])
                             (%x xs r. %T. if null T then [] 
                                           else f(x,hd T) # r(tl T)))(snd(S))"
 
+  zip       :: "'a list * 'b list => ('a*'b) list"
+  "zip      == zipWith  (%s. s)"
+
   unzip     :: "('a*'b) list => ('a list * 'b list)"
   "unzip    == foldr(% (a,b)(c,d).(a#c,b#d))([],[])"