src/HOLCF/ccc1.ML

--- a/src/HOLCF/ccc1.ML	Wed Jan 29 15:58:17 1997 +0100
+++ b/src/HOLCF/ccc1.ML	Fri Jan 31 13:57:33 1997 +0100
@@ -22,23 +22,19 @@
         (rtac refl 1)
         ]);
 
-qed_goalw "cfcomp1" ccc1.thy [oo_def] "(f oo g)=(LAM x.f`(g`x))"
- (fn prems =>
-        [
+qed_goalw "cfcomp1" ccc1.thy [oo_def] "(f oo g)=(LAM x.f`(g`x))" (fn _ => [
         (stac beta_cfun 1),
-        (cont_tacR 1),
+        (Simp_tac 1),
         (stac beta_cfun 1),
-        (cont_tacR 1),
-        (rtac refl 1)
+        (Simp_tac 1),
+	(rtac refl 1)
         ]);
 
-qed_goal "cfcomp2" ccc1.thy  "(f oo g)`x=f`(g`x)"
- (fn prems =>
-        [
+qed_goal "cfcomp2" ccc1.thy  "(f oo g)`x=f`(g`x)" (fn _ => [
         (stac cfcomp1 1),
         (stac beta_cfun 1),
-        (cont_tacR 1),
-        (rtac refl 1)
+        (Simp_tac 1),
+	(rtac refl 1)
         ]);