src/HOL/TLA/TLA.thy

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