--- a/src/HOLCF/One.ML Thu Jun 25 16:13:20 1998 +0200
+++ b/src/HOLCF/One.ML Thu Jun 25 16:28:41 1998 +0200
@@ -16,9 +16,8 @@
(fn prems =>
[
(lift.induct_tac "t" 1),
- (fast_tac HOL_cs 1),
(Simp_tac 1),
- (rtac unit_eq 1)
+ (Simp_tac 1)
]);
qed_goal "oneE" thy