diff -r 5f79a9e42507 -r a68f503805ed src/ZF/ex/LList.thy
--- a/src/ZF/ex/LList.thy	Fri Feb 18 16:36:42 2011 +0100
+++ b/src/ZF/ex/LList.thy	Fri Feb 18 17:03:30 2011 +0100
@@ -43,11 +43,9 @@
   lconst   :: "i => i"  where
   "lconst(a) == lfp(univ(a), %l. LCons(a,l))"
 
-consts
-  flip     :: "i => i"
-axioms
-  flip_LNil:   "flip(LNil) = LNil"
-
+axiomatization flip :: "i => i"
+where
+  flip_LNil:   "flip(LNil) = LNil" and
   flip_LCons:  "[| x \<in> bool; l \<in> llist(bool) |] 
                 ==> flip(LCons(x,l)) = LCons(not(x), flip(l))"