diff -r ae39b7b2a68a -r d97fa41cc600 src/HOL/TLA/Intensional.thy
--- a/src/HOL/TLA/Intensional.thy	Thu Jun 04 16:55:20 2009 +0200
+++ b/src/HOL/TLA/Intensional.thy	Fri Jun 05 08:00:53 2009 +0200
@@ -126,8 +126,8 @@
   "_liftLeq"      == "_lift2 (op <=)"
   "_liftMem"      == "_lift2 (op :)"
   "_liftNotMem x xs"   == "_liftNot (_liftMem x xs)"
-  "_liftFinset (_liftargs x xs)"  == "_lift2 insert x (_liftFinset xs)"
-  "_liftFinset x" == "_lift2 insert x (_const {})"
+  "_liftFinset (_liftargs x xs)"  == "_lift2 CONST insert x (_liftFinset xs)"
+  "_liftFinset x" == "_lift2 CONST insert x (_const {})"
   "_liftPair x (_liftargs y z)"       == "_liftPair x (_liftPair y z)"
   "_liftPair"     == "_lift2 Pair"
   "_liftCons"     == "lift2 Cons"