src/HOLCF/IMP/Denotational.ML

--- a/src/HOLCF/IMP/Denotational.ML	Mon Apr 27 16:46:56 1998 +0200
+++ b/src/HOLCF/IMP/Denotational.ML	Mon Apr 27 16:47:50 1998 +0200
@@ -18,7 +18,7 @@
 
 goalw thy [dlift_def]
  "(dlift f`l = Def y) = (? x. l = Def x & f`(Discr x) = Def y)";
-by (simp_tac (simpset() setloop (split_tac[expand_lift_case])) 1);
+by (simp_tac (simpset() addsplits [split_lift_case]) 1);
 qed "dlift_is_Def";
 Addsimps [dlift_is_Def];
 
@@ -33,13 +33,13 @@
     by (fast_tac ((HOL_cs addSIs evalc.intrs) addss simpset()) 1);
    by (fast_tac ((HOL_cs addSIs evalc.intrs) addss simpset()) 1);
   by (fast_tac ((HOL_cs addSIs evalc.intrs) addss simpset()) 1);
- by (simp_tac (simpset() setloop (split_tac[expand_if])) 1);
+ by (Simp_tac 1);
  by (fast_tac ((HOL_cs addIs evalc.intrs) addss simpset()) 1);
 by (Simp_tac 1);
 by (rtac fix_ind 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 (Simp_tac 1);
 by (safe_tac HOL_cs);
   by (fast_tac (HOL_cs addIs evalc.intrs) 1);
  by (fast_tac ((HOL_cs addSIs evalc.intrs) addss simpset()) 1);