# HG changeset patch
# User wenzelm
# Date 1248639853 -7200
# Node ID 6a6827bad05f446d4dbb9295c38659854e40748a
# Parent  f1b166317ae23e8965ff04b16d14d79e62bdd511
replaced old METAHYPS by FOCUS;

diff -r f1b166317ae2 -r 6a6827bad05f src/Provers/Arith/fast_lin_arith.ML
--- 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