src/HOL/Tools/Metis/metis_reconstruct.ML
changeset 58957 c9e744ea8a38
parent 58950 d07464875dd4
child 58963 26bf09b95dda
     1.1 --- a/src/HOL/Tools/Metis/metis_reconstruct.ML	Sun Nov 09 14:08:00 2014 +0100
     1.2 +++ b/src/HOL/Tools/Metis/metis_reconstruct.ML	Sun Nov 09 17:04:14 2014 +0100
     1.3 @@ -742,7 +742,7 @@
     1.4                THEN rename_tac outer_param_names 1
     1.5                THEN copy_prems_tac (map snd ax_counts) [] 1)
     1.6              THEN release_clusters_tac thy ax_counts substs ordered_clusters 1
     1.7 -            THEN match_tac [prems_imp_false] 1
     1.8 +            THEN match_tac ctxt' [prems_imp_false] 1
     1.9              THEN ALLGOALS (fn i => resolve_tac @{thms Meson.skolem_COMBK_I} i
    1.10                THEN rotate_tac (rotation_of_subgoal i) i
    1.11                THEN PRIMITIVE (unify_first_prem_with_concl thy i)