src/HOL/UNITY/Simple/Lift.ML

--- a/src/HOL/UNITY/Simple/Lift.ML	Mon Sep 30 16:12:16 2002 +0200
+++ b/src/HOL/UNITY/Simple/Lift.ML	Mon Sep 30 16:14:02 2002 +0200
@@ -205,7 +205,7 @@
   i.e. the trivial disjunction, leading to an asymmetrical proof.*)
 Goal "0<N ==> Req n Int {s. metric n s = N} <= goingup Un goingdown";
 by (Clarify_tac 1);
-by (auto_tac (claset(), metric_ss));
+by (force_tac (claset(), metric_ss) 1);
 qed "E_thm16c";