# HG changeset patch
# User paulson
# Date 818417825 -3600
# Node ID 48bcde67391b39b0728798daf4482446d454c15b
# Parent  7095d6b89734da19fc621ca67e62c27cb5cbb64b
Now def of apfst uses pattern-matching

diff -r 7095d6b89734 -r 48bcde67391b src/HOL/Univ.thy
--- a/src/HOL/Univ.thy	Fri Dec 08 10:47:25 1995 +0100
+++ b/src/HOL/Univ.thy	Fri Dec 08 11:17:05 1995 +0100
@@ -58,7 +58,7 @@
   Push_Node_def  "Push_Node == (%n x. Abs_Node (apfst (Push n) (Rep_Node x)))"
 
   (*crude "lists" of nats -- needed for the constructions*)
-  apfst_def  "apfst == (%f. split(%x y. (f(x),y)))"
+  apfst_def  "apfst == (%f (x,y). (f(x),y))"
   Push_def   "Push == (%b h. nat_case (Suc b) h)"
 
   (** operations on S-expressions -- sets of nodes **)