src/HOL/Univ.thy
changeset 1396 48bcde67391b
parent 1384 007ad29ce6ca
child 1475 7f5a4cd08209
     1.1 --- a/src/HOL/Univ.thy	Fri Dec 08 10:47:25 1995 +0100
     1.2 +++ b/src/HOL/Univ.thy	Fri Dec 08 11:17:05 1995 +0100
     1.3 @@ -58,7 +58,7 @@
     1.4    Push_Node_def  "Push_Node == (%n x. Abs_Node (apfst (Push n) (Rep_Node x)))"
     1.5  
     1.6    (*crude "lists" of nats -- needed for the constructions*)
     1.7 -  apfst_def  "apfst == (%f. split(%x y. (f(x),y)))"
     1.8 +  apfst_def  "apfst == (%f (x,y). (f(x),y))"
     1.9    Push_def   "Push == (%b h. nat_case (Suc b) h)"
    1.10  
    1.11    (** operations on S-expressions -- sets of nodes **)