src/HOLCF/Lift1.ML

--- a/src/HOLCF/Lift1.ML	Wed Jul 05 14:26:58 2000 +0200
+++ b/src/HOLCF/Lift1.ML	Wed Jul 05 16:37:52 2000 +0200
@@ -17,14 +17,12 @@
 by (fast_tac HOL_cs 1);
 qed"refl_less_lift";
 
-val prems = goalw thy [less_lift_def] 
+Goalw [less_lift_def] 
   "[|(x1::'a lift) << x2; x2 << x1|] ==> x1 = x2";
-by (cut_facts_tac prems 1);
 by (fast_tac HOL_cs 1);
 qed"antisym_less_lift";
 
-val prems = goalw Lift1.thy [less_lift_def] 
+Goalw [less_lift_def] 
   "[|(x1::'a lift) << x2; x2 << x3|] ==> x1 << x3";
-by (cut_facts_tac prems 1);
 by (fast_tac HOL_cs 1);
 qed"trans_less_lift";