--- a/src/HOL/Tools/record.ML Sun Jul 26 19:54:37 2009 +0200
+++ b/src/HOL/Tools/record.ML Sun Jul 26 20:38:11 2009 +0200
@@ -2161,7 +2161,7 @@
fn st => let val [s, s'] = map #1 (rev (Tactic.innermost_params 1 st)) in
st |> (res_inst_tac context [((rN, 0), s)] cases_scheme 1
THEN res_inst_tac context [((rN, 0), s')] cases_scheme 1
- THEN (METAHYPS equality_tac 1))
+ THEN (FOCUS (fn {prems, ...} => equality_tac prems) context 1))
(* simp_all_tac ss (sel_convs) would also work but is less efficient *)
end);
val equality = timeit_msg "record equality proof:" equality_prf;