diff -r 3fc2f9c40759 -r 0b9b8eb74101 List.thy
--- a/List.thy	Thu Aug 18 12:38:12 1994 +0200
+++ b/List.thy	Thu Aug 18 12:42:19 1994 +0200
@@ -21,33 +21,33 @@
 
 consts
 
-  List_Fun      :: "['a node set set, 'a node set set] => 'a node set set"
-  List          :: "'a node set set => 'a node set set"
-  Rep_List      :: "'a list => 'a node set"
-  Abs_List      :: "'a node set => 'a list"
-  NIL           :: "'a node set"
-  CONS          :: "['a node set, 'a node set] => 'a node set"
-  Nil           :: "'a list"
-  "#"           :: "['a, 'a list] => 'a list"                   (infixr 65)
-  List_case     :: "['a node set, 'b, ['a node set, 'a node set]=>'b] => 'b"
-  List_rec      :: "['a node set, 'b, ['a node set, 'a node set, 'b]=>'b] => 'b"
-  list_rec      :: "['a list, 'b, ['a, 'a list, 'b]=>'b] => 'b"
-  Rep_map       :: "('b => 'a node set) => ('b list => 'a node set)"
-  Abs_map       :: "('a node set => 'b) => 'a node set => 'b list"
-  null          :: "'a list => bool"
-  hd            :: "'a list => 'a"
-  tl,ttl        :: "'a list => 'a list"
+  List_Fun  :: "['a node set set, 'a node set set] => 'a node set set"
+  List      :: "'a node set set => 'a node set set"
+  Rep_List  :: "'a list => 'a node set"
+  Abs_List  :: "'a node set => 'a list"
+  NIL       :: "'a node set"
+  CONS      :: "['a node set, 'a node set] => 'a node set"
+  Nil       :: "'a list"
+  "#"       :: "['a, 'a list] => 'a list"                   	(infixr 65)
+  List_case :: "['b, ['a node set, 'a node set]=>'b, 'a node set] => 'b"
+  List_rec  :: "['a node set, 'b, ['a node set, 'a node set, 'b]=>'b] => 'b"
+  list_rec  :: "['a list, 'b, ['a, 'a list, 'b]=>'b] => 'b"
+  Rep_map   :: "('b => 'a node set) => ('b list => 'a node set)"
+  Abs_map   :: "('a node set => 'b) => 'a node set => 'b list"
+  null      :: "'a list => bool"
+  hd        :: "'a list => 'a"
+  tl,ttl    :: "'a list => 'a list"
   mem		:: "['a, 'a list] => bool"			(infixl 55)
-  list_all      :: "('a => bool) => ('a list => bool)"
-  map           :: "('a=>'b) => ('a list => 'b list)"
-  "@"		:: "['a list, 'a list] => 'a list"		(infixr 65)
-  list_case     :: "['a list, 'b, ['a, 'a list]=>'b] => 'b"
-  filter	:: "['a => bool, 'a list] => 'a list"
+  list_all  :: "('a => bool) => ('a list => bool)"
+  map       :: "('a=>'b) => ('a list => 'b list)"
+  "@"	    :: "['a list, 'a list] => 'a list"			(infixr 65)
+  list_case :: "['b, ['a, 'a list]=>'b, 'a list] => 'b"
+  filter    :: "['a => bool, 'a list] => 'a list"
 
   (* List Enumeration *)
 
-  "[]"          :: "'a list"                            ("[]")
-  "@List"       :: "args => 'a list"                    ("[(_)]")
+  "[]"      :: "'a list"                            ("[]")
+  "@List"   :: "args => 'a list"                    ("[(_)]")
 
   (* Special syntax for list_all and filter *)
   "@Alls"	:: "[idt, 'a list, bool] => bool"	("(2Alls _:_./ _)" 10)
@@ -58,7 +58,7 @@
   "[x]"         == "x#[]"
   "[]"          == "Nil"
 
-  "case xs of Nil => a | y#ys => b" == "list_case(xs,a,%y ys.b)"
+  "case xs of Nil => a | y#ys => b" == "list_case(a, %y ys.b, xs)"
 
   "[x:xs . P]"	== "filter(%x.P,xs)"
   "Alls x:xs.P"	== "list_all(%x.P,xs)"
@@ -84,13 +84,13 @@
   Nil_def       "Nil == Abs_List(NIL)"
   Cons_def      "x#xs == Abs_List(CONS(Leaf(x), Rep_List(xs)))"
 
-  List_case_def "List_case(M, c, d) == Case(M, %x.c, %u. Split(u, %x y.d(x, y)))"
+  List_case_def "List_case(c, d) == Case(%x.c, Split(d))"
 
   (* List Recursion -- the trancl is Essential; see list.ML *)
 
   List_rec_def
    "List_rec(M, c, d) == wfrec(trancl(pred_Sexp), M, \
-\                         %z g. List_case(z, c, %x y. d(x, y, g(y))))"
+\                         List_case(%g.c, %x y g. d(x, y, g(y))))"
 
   list_rec_def
    "list_rec(l, c, d) == \
@@ -115,6 +115,6 @@
   append_def	"xs@ys               == list_rec(xs, ys, %x l r. x#r)"
   filter_def	"filter(P,xs)        == \
 \                  list_rec(xs, [], %x xs r. if(P(x), x#r, r))"
-  list_case_def "list_case(xs, a, f) == list_rec(xs, a, %x xs r.f(x, xs))"
+  list_case_def "list_case(a, f, xs) == list_rec(xs, a, %x xs r.f(x, xs))"
 
 end