src/HOL/HOL.thy
changeset 58963 26bf09b95dda
parent 58958 114255dce178
child 59028 df7476e79558
     1.1 --- a/src/HOL/HOL.thy	Sun Nov 09 20:49:28 2014 +0100
     1.2 +++ b/src/HOL/HOL.thy	Mon Nov 10 21:49:48 2014 +0100
     1.3 @@ -1982,7 +1982,7 @@
     1.4      val filter_right = filter (not o wrong_prem o HOLogic.dest_Trueprop o hd o Thm.prems_of);
     1.5    in
     1.6      fun smp i = funpow i (fn m => filter_right ([spec] RL m)) ([mp]);
     1.7 -    fun smp_tac j = EVERY'[dresolve_tac (smp j), assume_tac];
     1.8 +    fun smp_tac ctxt j = EVERY'[dresolve_tac (smp j), assume_tac ctxt];
     1.9    end;
    1.10  
    1.11    local