# HG changeset patch
# User wenzelm
# Date 1316524050 -7200
# Node ID 8a4db903039fdd16fba0ebd1e5107db0e244194b
# Parent  99e1965f9c21e7a1cd41b5fdcfbea2ccc4dd32f3
proper fact binding;

diff -r 99e1965f9c21 -r 8a4db903039f src/CCL/ex/List.thy
--- a/src/CCL/ex/List.thy	Tue Sep 20 09:30:19 2011 +0200
+++ b/src/CCL/ex/List.thy	Tue Sep 20 15:07:30 2011 +0200
@@ -19,7 +19,7 @@
   where "l @ m == lrec(l,m,%x xs g. x$g)"
 
 axiomatization member :: "[i,i]=>i"  (infixr "mem" 55)  (* FIXME dangling eq *)
-  where "a mem l == lrec(l,false,%h t g. if eq(a,h) then true else g)"
+  where member_ax: "a mem l == lrec(l,false,%h t g. if eq(a,h) then true else g)"
 
 definition filter :: "[i,i]=>i"
   where "filter(f,l) == lrec(l,[],%x xs g. if f`x then x$g else g)"