src/HOL/Auth/OtwayReesBella.thy
changeset 51798 ad3a241def73
parent 51717 9e7d1c139569
child 58889 5b7a9633cfa8
     1.1 --- a/src/HOL/Auth/OtwayReesBella.thy	Sat Apr 27 11:37:50 2013 +0200
     1.2 +++ b/src/HOL/Auth/OtwayReesBella.thy	Sat Apr 27 20:50:20 2013 +0200
     1.3 @@ -258,9 +258,9 @@
     1.4  
     1.5  method_setup disentangle = {*
     1.6      Scan.succeed
     1.7 -     (K (SIMPLE_METHOD
     1.8 +     (fn ctxt => SIMPLE_METHOD
     1.9        (REPEAT_FIRST (eresolve_tac [asm_rl, conjE, disjE] 
    1.10 -                   ORELSE' hyp_subst_tac)))) *}
    1.11 +                   ORELSE' hyp_subst_tac ctxt))) *}
    1.12    "for eliminating conjunctions, disjunctions and the like"
    1.13  
    1.14