Mercurialisabelle / diff
summary | shortlog | changelog | graph | tags | branches | files | changeset | file | revisions | annotate | diff | raw
src/HOL/Library/Old_SMT/old_z3_proof_methods.ML
changeset 58957 c9e744ea8a38
parent 58058 1a0b18176548
child 59058 a78612c67ec0 
     1.1 --- a/src/HOL/Library/Old_SMT/old_z3_proof_methods.ML	Sun Nov 09 14:08:00 2014 +0100
     1.2 +++ b/src/HOL/Library/Old_SMT/old_z3_proof_methods.ML	Sun Nov 09 17:04:14 2014 +0100
     1.3 @@ -80,7 +80,7 @@
     1.4  fun prove_rhs ctxt def lhs =
     1.5    Old_Z3_Proof_Tools.by_tac ctxt (
     1.6      CONVERSION (Conv.top_sweep_conv (K (Conv.rewr_conv def)) ctxt)
     1.7 -    THEN' REPEAT_ALL_NEW (match_tac @{thms allI})
     1.8 +    THEN' REPEAT_ALL_NEW (match_tac ctxt @{thms allI})
     1.9      THEN' rtac (@{thm inv_f_f} OF [prove_inj_prop ctxt def lhs]))
    1.10  
    1.11
isabelle