diff -r fe5b796d6b2a -r 23b67731f4f0 src/HOL/TLA/TLA.thy
--- a/src/HOL/TLA/TLA.thy	Mon Mar 23 10:16:20 2015 +0100
+++ b/src/HOL/TLA/TLA.thy	Mon Mar 23 13:30:59 2015 +0100
@@ -300,15 +300,15 @@
 
 fun merge_temp_box_tac ctxt i =
   REPEAT_DETERM (EVERY [etac @{thm box_conjE_temp} i, atac i,
-    Rule_Insts.eres_inst_tac ctxt [((("'a", 0), Position.none), "behavior")] @{thm box_thin} i])
+    Rule_Insts.eres_inst_tac ctxt [((("'a", 0), Position.none), "behavior")] [] @{thm box_thin} i])
 
 fun merge_stp_box_tac ctxt i =
   REPEAT_DETERM (EVERY [etac @{thm box_conjE_stp} i, atac i,
-    Rule_Insts.eres_inst_tac ctxt [((("'a", 0), Position.none), "state")] @{thm box_thin} i])
+    Rule_Insts.eres_inst_tac ctxt [((("'a", 0), Position.none), "state")] [] @{thm box_thin} i])
 
 fun merge_act_box_tac ctxt i =
   REPEAT_DETERM (EVERY [etac @{thm box_conjE_act} i, atac i,
-    Rule_Insts.eres_inst_tac ctxt [((("'a", 0), Position.none), "state * state")] @{thm box_thin} i])
+    Rule_Insts.eres_inst_tac ctxt [((("'a", 0), Position.none), "state * state")] [] @{thm box_thin} i])
 *}
 
 method_setup merge_box = {* Scan.succeed (K (SIMPLE_METHOD' merge_box_tac)) *}