diff -r 6b26b886ff69 -r 4e4ee8a101be src/HOLCF/IMP/Denotational.ML
--- a/src/HOLCF/IMP/Denotational.ML	Sun May 25 16:17:09 1997 +0200
+++ b/src/HOLCF/IMP/Denotational.ML	Sun May 25 16:57:19 1997 +0200
@@ -37,7 +37,7 @@
  by (fast_tac ((HOL_cs addIs evalc.intrs) addss !simpset) 1);
 by (Simp_tac 1);
 br fix_ind 1;
-  by(fast_tac (HOL_cs addSIs (adm_lemmas@[adm_chfindom,flat_lift])) 1);
+  by(fast_tac (HOL_cs addSIs (adm_lemmas@[adm_chfindom,ax_flat_lift])) 1);
  by (Simp_tac 1);
 by (simp_tac (!simpset setloop (split_tac[expand_if])) 1);
 by (safe_tac HOL_cs);