src/HOL/Auth/OtwayReesBella.thy

--- a/src/HOL/Auth/OtwayReesBella.thy	Sat Apr 27 11:37:50 2013 +0200
+++ b/src/HOL/Auth/OtwayReesBella.thy	Sat Apr 27 20:50:20 2013 +0200
@@ -258,9 +258,9 @@
 
 method_setup disentangle = {*
     Scan.succeed
-     (K (SIMPLE_METHOD
+     (fn ctxt => SIMPLE_METHOD
       (REPEAT_FIRST (eresolve_tac [asm_rl, conjE, disjE] 
-                   ORELSE' hyp_subst_tac)))) *}
+                   ORELSE' hyp_subst_tac ctxt))) *}
   "for eliminating conjunctions, disjunctions and the like"