--- 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"