--- a/src/HOL/Tools/record.ML Sun Nov 09 20:49:28 2014 +0100
+++ b/src/HOL/Tools/record.ML Mon Nov 10 21:49:48 2014 +0100
@@ -1625,9 +1625,9 @@
(fn {context = ctxt, ...} =>
EVERY1
[rtac @{thm equal_intr_rule}, Goal.norm_hhf_tac ctxt,
- etac @{thm meta_allE}, atac,
+ etac @{thm meta_allE}, assume_tac ctxt,
rtac (@{thm prop_subst} OF [surject]),
- REPEAT o etac @{thm meta_allE}, atac]));
+ REPEAT o etac @{thm meta_allE}, assume_tac ctxt]));
val induct = timeit_msg ctxt "record extension induct proof:" (fn () =>
let val (assm, concl) = induct_prop in
@@ -2160,9 +2160,9 @@
(fn {context = ctxt', ...} =>
EVERY1
[rtac @{thm equal_intr_rule}, Goal.norm_hhf_tac ctxt',
- etac @{thm meta_allE}, atac,
+ etac @{thm meta_allE}, assume_tac ctxt',
rtac (@{thm prop_subst} OF [surjective]),
- REPEAT o etac @{thm meta_allE}, atac]));
+ REPEAT o etac @{thm meta_allE}, assume_tac ctxt']));
val split_object = timeit_msg ctxt "record split_object proof:" (fn () =>
Goal.prove_sorry_global defs_thy [] [] split_object_prop