changeset 58957 | c9e744ea8a38 |
parent 58058 | 1a0b18176548 |
child 59058 | a78612c67ec0 |
--- a/src/HOL/Library/Old_SMT/old_z3_proof_methods.ML Sun Nov 09 14:08:00 2014 +0100 +++ b/src/HOL/Library/Old_SMT/old_z3_proof_methods.ML Sun Nov 09 17:04:14 2014 +0100 @@ -80,7 +80,7 @@ fun prove_rhs ctxt def lhs = Old_Z3_Proof_Tools.by_tac ctxt ( CONVERSION (Conv.top_sweep_conv (K (Conv.rewr_conv def)) ctxt) - THEN' REPEAT_ALL_NEW (match_tac @{thms allI}) + THEN' REPEAT_ALL_NEW (match_tac ctxt @{thms allI}) THEN' rtac (@{thm inv_f_f} OF [prove_inj_prop ctxt def lhs]))