fixed unit_eq;

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