src/HOL/TLA/TLA.thy
changeset 59780 23b67731f4f0
parent 59763 56d2c357e6b5
child 60587 0318b43ee95c
     1.1 --- a/src/HOL/TLA/TLA.thy	Mon Mar 23 10:16:20 2015 +0100
     1.2 +++ b/src/HOL/TLA/TLA.thy	Mon Mar 23 13:30:59 2015 +0100
     1.3 @@ -300,15 +300,15 @@
     1.4  
     1.5  fun merge_temp_box_tac ctxt i =
     1.6    REPEAT_DETERM (EVERY [etac @{thm box_conjE_temp} i, atac i,
     1.7 -    Rule_Insts.eres_inst_tac ctxt [((("'a", 0), Position.none), "behavior")] @{thm box_thin} i])
     1.8 +    Rule_Insts.eres_inst_tac ctxt [((("'a", 0), Position.none), "behavior")] [] @{thm box_thin} i])
     1.9  
    1.10  fun merge_stp_box_tac ctxt i =
    1.11    REPEAT_DETERM (EVERY [etac @{thm box_conjE_stp} i, atac i,
    1.12 -    Rule_Insts.eres_inst_tac ctxt [((("'a", 0), Position.none), "state")] @{thm box_thin} i])
    1.13 +    Rule_Insts.eres_inst_tac ctxt [((("'a", 0), Position.none), "state")] [] @{thm box_thin} i])
    1.14  
    1.15  fun merge_act_box_tac ctxt i =
    1.16    REPEAT_DETERM (EVERY [etac @{thm box_conjE_act} i, atac i,
    1.17 -    Rule_Insts.eres_inst_tac ctxt [((("'a", 0), Position.none), "state * state")] @{thm box_thin} i])
    1.18 +    Rule_Insts.eres_inst_tac ctxt [((("'a", 0), Position.none), "state * state")] [] @{thm box_thin} i])
    1.19  *}
    1.20  
    1.21  method_setup merge_box = {* Scan.succeed (K (SIMPLE_METHOD' merge_box_tac)) *}