--- a/src/Provers/Arith/fast_lin_arith.ML Sun Jul 26 20:57:19 2009 +0200
+++ b/src/Provers/Arith/fast_lin_arith.ML Sun Jul 26 22:24:13 2009 +0200
@@ -788,7 +788,7 @@
all_tac) THEN
PRIMITIVE (trace_thm ctxt "State after neqE:") THEN
(* use theorems generated from the actual justifications *)
- METAHYPS (fn asms => rtac (mkthm ss asms j) 1) i
+ FOCUS (fn {prems, ...} => rtac (mkthm ss prems j) 1) ctxt i
in
(* rewrite "[| A1; ...; An |] ==> B" to "[| A1; ...; An; ~B |] ==> False" *)
DETERM (resolve_tac [LA_Logic.notI, LA_Logic.ccontr] i) THEN