1.1 --- a/src/HOL/Tools/record.ML	Wed Jan 11 16:23:59 2012 +0100
     1.2 +++ b/src/HOL/Tools/record.ML	Wed Jan 11 16:25:34 2012 +0100
     1.3 @@ -1630,7 +1630,7 @@
     1.4        Skip_Proof.prove_global defs_thy [] [] split_meta_prop
     1.5          (fn _ =>
     1.6            EVERY1
     1.7 -           [rtac equal_intr_rule, Goal.norm_hhf_tac,
     1.8 +           [rtac @{thm equal_intr_rule}, Goal.norm_hhf_tac,
     1.9              etac @{thm meta_allE}, atac,
    1.10              rtac (@{thm prop_subst} OF [surject]),
    1.11              REPEAT o etac @{thm meta_allE}, atac]));
    1.12 @@ -2155,7 +2155,7 @@
    1.13        Skip_Proof.prove_global defs_thy [] [] split_meta_prop
    1.14          (fn _ =>
    1.15            EVERY1
    1.16 -           [rtac equal_intr_rule, Goal.norm_hhf_tac,
    1.17 +           [rtac @{thm equal_intr_rule}, Goal.norm_hhf_tac,
    1.18              etac @{thm meta_allE}, atac,
    1.19              rtac (@{thm prop_subst} OF [surjective]),
    1.20              REPEAT o etac @{thm meta_allE}, atac]));