src/HOL/HOLCF/Tr.thy
changeset 58956 a816aa3ff391
parent 58880 0baae4311a9f
child 62175 8ffc4d0e652d
     1.1 --- a/src/HOL/HOLCF/Tr.thy	Sun Nov 09 11:05:20 2014 +0100
     1.2 +++ b/src/HOL/HOLCF/Tr.thy	Sun Nov 09 14:08:00 2014 +0100
     1.3 @@ -154,7 +154,7 @@
     1.4  ML {*
     1.5  fun split_If_tac ctxt =
     1.6    simp_tac (put_simpset HOL_basic_ss ctxt addsimps [@{thm If2_def} RS sym])
     1.7 -    THEN' (split_tac [@{thm split_If2}])
     1.8 +    THEN' (split_tac ctxt [@{thm split_If2}])
     1.9  *}
    1.10  
    1.11  subsection "Rewriting of HOLCF operations to HOL functions"