1.1 --- a/src/HOL/TLA/TLA.thy	Tue Feb 10 14:29:36 2015 +0100
     1.2 +++ b/src/HOL/TLA/TLA.thy	Tue Feb 10 14:48:26 2015 +0100
     1.3 @@ -697,7 +697,8 @@
     1.4  
     1.5  (* A tactic that "boxes" all fairness conditions. Apply more_temp_simps to "unbox". *)
     1.6  ML {*
     1.7 -val box_fair_tac = SELECT_GOAL (REPEAT (dresolve_tac [@{thm BoxWFI}, @{thm BoxSFI}] 1))
     1.8 +fun box_fair_tac ctxt =
     1.9 +  SELECT_GOAL (REPEAT (dresolve_tac ctxt [@{thm BoxWFI}, @{thm BoxSFI}] 1))
    1.10  *}
    1.11  
    1.12